%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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\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 %% 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.$}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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\modulo{{\rm mod~}} \def\std{{\rm std}} \def\Re{{\rm Re}} \def\Im{{\rm Im}} \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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\input smallfonts.tex %\input param.2 %\input fonts.5b %\input symbols.1 %\input titles.6c %\input macros.18 % \font\tenib=cmmib10 \def\bmf{{\hbox{\tenib f}}} \def\bmD{{\hbox{\tenib D}}} \def\bmv{{\hbox{\tenib v}}} % \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\ssB{{\scriptscriptstyle B}} \def\ssF{{\scriptscriptstyle F}} \def\ssG{{\scriptscriptstyle G}} \def\ssH{{\scriptscriptstyle H}} \def\ssL{{\scriptscriptstyle L}} \def\ssN{{\scriptscriptstyle N}} \def\ssT{{\scriptscriptstyle T}} \def\ssTp{{\scriptscriptstyle T'}} \def\ssY{{\scriptscriptstyle Y}} \def\ssZ{{\scriptscriptstyle Z}} \def\ssKK{{\scriptscriptstyle\KK}} \def\ssnatural{{\scriptscriptstyle\natural}} \def\ssinteger{{\scriptscriptstyle\integer}} \def\Int{\int\limits} \def\bdot{\hbox{\bf .}} \def\ldot{\,.} \def\Lplus{L^{^{+}}} \def\Lminus{L^{^{-}}} \def\std{{\rm std}} \def\LKS{{\Bbb L}} \let\Poinc\Psi \let\Flow\Phi %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \addref{M} \addref{CCP} \addref{KT} \addref{S} \addref{KNS} \addref{JKT} \addref{Il} \addref{CEES} \addref{D} \addref{ZM} \addref{ZMb} \addref{Z} \addref{AZ} \addref{ZG} \addref{GZ} \addref{AKT} \addref{AK} \addref{DS} \addref{Pazy} \addref{IEEE} \addref{Ada} \addref{Files} \addref{Gnat} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \def\leftheadline{\sevenrm\hfil GIANNI ARIOLI and HANS KOCH\hfil} \def\rightheadline{\sevenrm\hfil Integration of dissipative PDEs: a case study\hfil} %% \cl{{\magtenbf Integration of dissipative PDEs: a case study}} \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 develop a computer-assisted technique to construct and analyze orbits of dissipative evolution equations. As a case study, the methods are applied to the Kuramoto-Sivashinski equation. We prove the existence of a hyperbolic periodic orbit. \section Introduction %%%%%%%%%%%%%%%%%%%%% In this paper we consider the problem of investigating the flow of dissipative parabolic equations via computer-assisted methods. The type of equations that we have in mind are of the form $$ \partial_t u+(i\partial_x)^m u +H(u,\partial_x u,\ldots,\partial_x^{m-1}u)=0\,, \equation(genForm) $$ with $m>0$ even, $H$ real analytic, and $u=u(t,x)$ satisfying suitable boundary conditions on a bounded spatial domain. Our goal is to obtain estimates for the time-$t$ map and its derivative, for small times $t>0$, and to combine these estimates with shadowing arguments, in order to control the long-time dynamics. For periodic orbits, this includes bounds on the eigenvalues of the linearized return map. Our method takes advantage of the fact that the solutions $u(t,x)$ of equation \equ(genForm) are real analytic in $x$, when $t>0$, due to the dissipation and the analyticity of $H$. This allows us to obtain accurate bounds in a relatively straightforward and general way. As a case study, we consider the unidimensional Kuramoto-Sivashinski equation, which has been the focus of numerous analytical and numerical investigations [\rKT--\rZMb]. Considering Dirichlet boundary conditions on $[0,\pi]$, this equation can be written in the form $$ \eqalign{ \partial_tu+4\partial_x^4u+\alpha\bigl(\partial_x^2u +2u\partial_xu\bigr)&=0\,,\cr u(t,0)=u(t,\pi)&=0\,,\cr} \qquad x\in[0,\pi]\,,\quad t\in\real\,. \equation(ks) $$ It is a well known numerical result [\rCCP] that this system exhibits chaotic dynamics when $\alpha>133$. Obtaining rigorous bounds for such large values of $\alpha$ is more difficult, since high frequency modes contribute more heavily to the dynamics. In order to test the robustness of our algorithm, and to make a first step towards the analysis of chaotic dynamics, we consider the value $\alpha=150$, which is well above the chaotic threshold. Our main result on the Kuramoto-Sivashinski equation is the following. \claim Theorem(Main) Equation \equ(ks) with $\alpha=150$ admits a hyperbolic periodic orbit of period $\tau=0.00214688\dots$. The Poincar\'e map associated with some transversal hyperplane is compact, and its eigenvalues lie in the disk $|\mu|<0.69$, except for a simple eigenvalue $|\mu_1|>4.8$. Somewhat similar results were obtained recently in [\rZ], namely the existence of periodic orbits, for several values of $\alpha$ between $30$ and $134$. However, the methods used in [\rZ] are purely topological and given no information on the stability of the orbit. The remaining part of the paper is structured as follows. In Section 2, we outline the general strategy and then describe the various steps in more detail. This part applies to dynamical systems in any separable Banach space, although the approach is motivated by the intended applications. A more specific functional setting is introduced in Section 3, where we discuss the integral equation used to control the time-$t$ map. Section 4 describes our implementation of the various steps, and further details of our computer-assisted proof. \section Strategy and techniques %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Consider an evolution equation of the type $$ \partial_t u=Lu+G(u)\,,\qquad u(0)=\nu\,, \equation(KStypeOne) $$ for a function $u=u(t)$, defined for $t\in[0,\infty)$, that takes values in some Banach space $\XX$. Here, $L$ and $G$ are operators on $\XX$, with $L$ linear. In the applications that we have in mind, which include the Kuramoto-Sivashinski equation, $\XX$ is a space of real-valued functions on a bounded domain in $\real^n$, satisfying suitable boundary conditions. Assume that we can compute numerically an approximate periodic orbit $\bar u$, starting at some point $\bar u_0$ at time $t=0$, and returning to the same point at a later time $t=\bar\tau$. After choosing a codimension-one hyperplane $S_0\subset\XX$ that intersects the curve $\bar u$ transversally at $\bar u_0\,$, we define the corresponding Poincar\'e return map $\Poinc: S_0\to S_0\,$, by setting $\Poinc(u)=u(t)$, where $t=t(\bar u_0)$ is the first return time to the section $S_0\,$. Here, and in what follows, a Poincar\'e return map need only be defined locally. If the system is dissipative, then the derivative of $\Poinc$ is compact, and in particular, it has only finitely many eigenvalues of modulus larger than $1$. We will refer to the corresponding eigenvectors as the ``expanding directions''. Our strategy for proving the existence of hyperbolic orbits involves several steps and technical tools. The basic tool is a computer-assisted technique for computing bounds on the time-$t$ map $\Flow_t$ of the system, and of its derivative $D\Flow_t\,$. Then we choose a sequence of intermediate Poincar\'e sections $S_j$ along the approximate orbit and compute rigorous estimates on the intermediate Poincar\'e maps $P_j: S_{j-1}\to S_j$ and their derivatives. By means of a shadowing technique, applied to the sequence of map $P_j\,$, we prove the existence of a true periodic orbit close to $\bar u$. This information is then used to estimate the derivatives of the intermediate Poincar\'e maps $P_j\,$. After verifying appropriate cone conditions for these derivatives, we obtain the desired bounds on the full Poincar\'e map. \subsection Integration %%%%%%%%%%%%%%%%%%%%%%% Our first goal is to integrate equation \equ(KStypeOne) on a sequence of time intervals $[T_{n-1},T_n]$, starting with $T_0=0$. Since the problem is autonomous, it suffices to consider the initial value problem on $[0,T]$. We turn \equ(KStypeOne) into an integral equation as usual, by rewriting the equation as $$ \partial_t\left[e^{-tL}u\right]=e^{-tL}G(u)\,,\qquad u(0)=\nu\,, \equation(KStypeThree) $$ integrating both sides, and then multiplying by $e^{tL}$, $$ u(t)=e^{tL}\nu +\int_0^t e^{(t-s)L}G(u(s))\,ds\,,\qquad 0\le t\le T\,. \equation(KStypeFour) $$ After defining a Banach space $\XX$ of admissible initial conditions $\nu$, our aim is to solve equation \equ(KStypeFour) by iteration, on a Banach space $\XX_\ssT$ of continuous $\XX$-valued functions on the interval $J=[0,T]$. Setting $\Flow_t(\nu)=u(t)$ then defines the time-$t$ map $\Flow_t$ on $\XX$, for $t\in J$. To be more precise, suppose that $L$ has a compact inverse, and a sequence of eigenvectors $\bmv_1,\bmv_2,\dots$ whose span is dense in $\XX$. Let $-\lambda_1,-\lambda_2,\ldots$ be the corresponding eigenvalues, and assume that $\lambda_k>0$ for sufficiently large $k$. Then $t\mapsto e^{tL}$ is a continuous semigroup on $\XX$. Substituting the formal expansion $u(t)=\sum_k u_k(t)\bmv_k$ into equation \equ(KStypeFour) yields a system of (infinitely many) coupled ODEs $$ u_k(t)=e^{-\lambda_kt}\nu_k +\int_0^te^{-\lambda_k(t-s)}g_k(s)\,ds\,,\qquad t\in J\,, \equation(KStypeFive) $$ where $\{\nu_k\}$ and $\{g_k(t)\}$ are the expansion coefficients for the vectors $\nu$ and $g(t)=G(u(t))$, respectively. Our aim is to work with a finite truncation of this system of ODEs, say $k\le N$, and to control the truncation errors. The truncation is defined in terms of the spectral projection $\proj_\ssL$ onto the span of the first $N$ eigenvectors of $L$. The same approach will be used to analyze the derivative $D\Flow_t$ of the time-$t$ map: The function $w=D\Flow_t(u)\omega$ is the solution of the initial value problem $$ \partial_t w=Lw+DG(u)w\,,\qquad w(0)=\omega\,, \equation(KSvar) $$ which can be reduced to an integral equations similar to \equ(KStypeFour) and \equ(KStypeFive). Further details are provided in Section 3. \subsection Intermediate Poincar\'e maps %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% A well known problem with computer-assisted integration is that the errors accumulate along the orbit, making the computation useless after a certain amount of time. In our approach to the Kuramoto-Sivashinski equation, this time is significantly shorter than what would be needed to estimate the Poincar\'e map $\Poinc$ directly. (And we do not expect the situation to be much better with other PDEs.) Adapting an approach that has been developed for finite dimensional dynamical systems [\rAZ], we proceed by smaller time steps as follows. Consider a partition of the approximate period $[0,\bar\tau]$ into $M$ subintervals $[t_j,t_{j+1}]$, where $t_j=j\bar\tau/M$ for $j=0,1,\ldots,M$. Then the points $\bar u_j=\bar u(t_j)$ define a discretization of the approximate orbit $\bar u$. For each $j$, we choose a nonzero functional $\eta_j:\XX\to\real$ and define a Poincar\'e section $S_j=\bar u_j+X_j\,$, where $X_j$ is the null space of $\eta_j\,$. After verifying that $S_j$ is transversal to the flow, as defined below, a Poincar\'e map $P_j:S_{j-1}\to S_j$ is defined in the usual way as $x\mapsto\Flow_t(x)$, where $t=t(x)$ is the smallest positive number such that $\Flow_t(x)\in S_j\,$. The composition of all these ``intermediate'' Poincar\'e maps yields the full local Poincar\'e map $\Poinc$. In our implementation of this procedure, we choose for each $j$ an ordered basis in $\proj_\ssL\XX$. The second basis vector is chosen to point roughly in the direction of the flow at $\bar u_j\,$. Then we define $\eta_j(x)$ to be the second coordinate of $\proj_\ssL(x-\bar u_j)$. We will use (verify) the following notion of transversality. Let $B\subset\XX$ be a fixed set of initial conditions. Assume that $\eta:\XX\to\real$ is continuous and nonzero. \claim Definition(transversal) Consider a differentiable flow $(t,\nu)\mapsto u(t)$, defined on $[a,c]\times B$. Let $s\in\real$. We say that the section $S=\eta^{-1}(s)$ is transversal to the flow if, for all initial conditions $\nu\in B$, the interval bounded by $\eta(u(a))$ and $\eta(u(c))$ contains $s$, and the derivative of $t\mapsto\eta(u(t))$ is bounded away from zero on $[a,c]$, uniformly in $\nu$. \subsection Shadowing %%%%%%%%%%%%%%%%%%%%% Our aim is to prove that there exists a true orbit that closely ``shadows'' the approximate orbit $\bar u$. In addition, we would like to show that the full Poincar\'e map has no eigenvalue on the unit circle, and to estimate the spectral gap between the least expanding and least contracting eigenvalue. Our main tool for the first step is Theorem 2.1 below, which is an extension to the infinite dimensional setting of Theorem 4 in [\rZG]. (See also [\rZ] for an approach to the infinite dimensional case.) \claim Theorem(fpt) Consider a Banach space $X=\real\oplus Z$, and let $V$ be the closed unit ball in $Z$. Let $F$ be a continuous and compact map from $[-1,1]\times V$ to $X=\real\oplus Z$. Writing $F(u,v)=(g(u,v),h(u,v))$, assume that $g(-1,v)\le -1$ and $g(1,v)\ge 1$ and $\|h(u,v)\|\le 1$, for all $u\in[-1,1]$ and $v\in V$. Then $F$ has a fixed point in $[-1,1]\times V$. \proof We may assume that the norm on $X$ is given by $\|(u,v)\|=\max\{|u|,\|v\|\}$. By our assumption on $F$, the closure $K$ of $F([1,1]\times V)$ is compact. Thus, given $\eps>0$, there exist points $w_1,w_2,\ldots w_n\in K$, such that the balls $W_i=\{w\in X: \|w-w_i\|<\eps\}$ cover the set $K$. For $w\in K$ define $$ \phi_\eps(w) ={\sum_{i=1}^n\varphi_i(w)w_i\over\sum_{i=1}^n\varphi_i(w)}\,,\qquad \varphi_i(w) =\cases{\eps-\|w-w_i\| &if $w\in W_i\,$;\cr 0 &otherwise.\cr} $$ Clearly, $\phi_\eps: K\to X$ is continuous, and $\|\phi_\eps(w)-w\|\le\eps$ for all $w\in K$. Assuming $\eps<\half$, define $\psi_\eps(u,v)=((1+2\eps)u,(1-2\eps)v)$. Then $F_\eps=\psi_\eps\circ\phi_\eps\circ F$ is continuous on $[-1,1]\times V$ and satisfies $\|F(x)-F_\eps(x)\|\le c\eps$, for some fixed constant $c>0$. Denote by $X_\eps$ the subspace of $X$ spanned by the vectors $\{w_0,w_1,\ldots,w_n\}$, where $w_0=(1,0)$. Notice that $F_\eps$ takes values in $X_\eps\,$. The restriction of $F_\eps$ to $X_\eps$ satisfies the hypotheses of Theorem 4 in [\rZG], and therefore it admits a fixed point in $[-1,1]\times V$. If $x_m$ is such a fixed point, obtained with $\eps\le{1\over cm}$, then $\|F(x_m)-x_m\|=\|F(x_m)-F_\eps(x_m)\|\le{1\over m}$. Since $F$ is compact, we can choose $m\mapsto x_m$ in such a way that $F(x_m)\to x$ for some $x$ in $[-1,1]\times V$. Then $$ \|x-x_m\| \le\|x-F(x_m)\|+\|F(x_m)-x_m\|\to 0\,. $$ Thus, $x_m\to x$, and $F(x)=\lim_{m\to\infty}F(x_m)=x$ by the continuity of $F$. \qed In order to apply \clm(fpt) to the sequence of Poincar\'e maps described in the previous subsection we use the following definitions, which are analogues of similar definitions in [\rAZ,\rZG,\rGZ]. Assume that $\XX=\YY\oplus\Theta\oplus\ZZ$, where $\YY$ and $\Theta$ are one-dimensional subspaces of $\XX$. Denote by $U$ and $V$ the closed unit balls in $\YY$ and $\ZZ$, respectively. \claim Definition(Abox) A section (of $\XX$) is codimension-one affine subspace of $\XX$. A box in a section $S$ is the image of $U\times V$ under a bi-continuous affine map $\psi:\YY\times\ZZ\to S$. \claim Definition(cover) Let $B_1=\psi_1(U\times V)$ and $B_2=\psi_2(U\times V)$ be boxes in two section $S_1$ and $S_2\,$, respectively. Given a map $f: B_1\to S_2\,$, we say that $B_1$ $f$-covers $B_2$ if the map $F:U\times V\to\YY\times\ZZ$, defined by $F=\psi_2^{-1}\circ f\circ\psi_1\,$, satisfies the hypotheses of \clm(fpt). For simplicity, we identified here $\YY$ with $\real$, and $U$ with $[-1,1]$. Roughly speaking, the set $B_1$ is stretched along $B_2$ in the direction $\psi_1(U)$ and compressed in the other directions by the map $f$. Clearly, this definition could be extended to a larger number of expanding directions. Consider now the Poincar\'e maps $P_j: S_{j-1}\to S_j$ described in Subsection 2.2, and for each $j$, let $B_j$ be a box in $S_j\,$. By periodicity, we identify $j=M$ with $j=0$. \claim Corollary(fpt2) If for each $j$, the box $B_{j-1}$ $P_j$-covers $B_j\,$, then the Poincar\'e map $\Poinc:S_0\to S_0\,$, defined by $\Poinc=P_M\circ\dots\circ P_2\circ P_1\,$, has a fixed point in $B_0\,$. \subsection Derivatives of the Poincar\'e map %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% In our application of \clm(fpt2), we estimate the image of a box $B_j$ under the flow via bounds on the derivative of the flow. The same bounds can also be used to prove hyperbolicity. To be more specific, let $u$ be a periodic orbit, denote by $u_j$ its intersection with the section $S_j\,$, and define $\dot u_j=Lu_j+G(u_j)$, for all $j$. A simple calculation shows that $$ DP_j(u_{j-1})w=D\Flow_{t(u_{j-1})}(u_{j-1})w -{\eta_j(D\Flow_{t(u_{j-1})}(u_{j-1})w)\over\eta_j(\dot u_j)}\dot u_j\,. \equation(DerPmap) $$ Thus, what we need are accurate estimates on the velocities $\dot u_j\,$. The low-frequency parts $\ell_j=\proj_\ssL\dot u_j$ are estimated explicitly in our construction of the orbit, since $G(u(s))$ appears in the integral equation \equ(KStypeFour), and $\ell_j=\proj_\ssL G(u_j)$. Consider now the high-frequency part $h_j=\proj_\ssH\dot u_j\,$. Here, and in what follows, $\proj_\ssH=\Id-\proj_\ssL\,$. After proving that $\dot u_j\in\XX$ for all $j$, we can use that $\dot u_j=D\Flow_{t(u_{j-1})}(u_{j-1})\dot u_{j-1}\,$. This immediately yields the following \claim Proposition(EstVel) Let $k_j=\proj_\ssH D\Flow_{t(u_{j-1})}(u_{j-1})\ell_{j-1}$ and $D_j=\proj_\ssH D\Flow_{t(u_{j-1})}(u_{j-1})\proj_\ssH\,$. Then $$ \|h_j\|\le \|k_j\|+\|D_j\|\|h_{j-1}\|\,,\qquad j=1,2,\ldots,M. $$ In particular, if $\|k_j\|\le b$ and $\|D_j\|\le a<1$ for all $j$, then $\|h_j\|\le(1-a)^{-1}b$. \subsection Hyperbolicity %%%%%%%%%%%%%%%%%%%%%%%%% In order to compute a lower bound on the modulus of the expanding eigenvalue of $D\Poinc(u_0)$, and an upper bound on the moduli of the contracting eigenvalues, we replace the $P_j$-covering conditions by cone conditions on the derivatives $DP_j\,$. This corresponds roughly to replacing \clm(fpt) by the following theorem. \claim Theorem(eig) Let $A\not=0$ be a bounded linear operator on a real Banach space $X=Y\oplus Z$, with $Y$ one-dimensional. Thus, if $y\in Y$ and $z\in Z$, we have a unique decomposition $$ A(y+z)=y'+z'\,,\qquad y'\in Y,\ z'\in Z\,. \equation(expansion) $$ Assume now that $A$ is compact, and that there exist positive real numbers $\beta<\alpha$, such that $\|z'\|\le\beta\max\{\|y\|,\|z\|\}$, and such that $\|y'\|\ge\alpha\|y\|$ whenever $\|y\|\ge\|z\|$. Then $A$ has a simple eigenvalue $\lambda$ of modulus $|\lambda|\ge\alpha$, and no other eigenvalue of modulus $>\beta$. \proof Consider the double cone $\CC$, defined by $\|y\|\ge\|z\|$. It is preserved by $A$. For any $x=y+z$ in $\CC$ we have $\|y'\|\ge\alpha\|y\|$, and thus $\|A^n x\|\ge c\alpha^n$ for all $n\ge 0$, with $c>0$. This guarantees e.g.~that $A$ has a spectral radius $\rho(A)\ge\alpha$. Let $\lambda$ be an eigenvalue of $A$, and let $\bar x=\bar y+\bar z$ be an eigenvector for this eigenvalue. If $|\lambda|<\alpha$, then $\bar x$ cannot belong to $C$, since $\|A^n\bar x\|$ grows slower than $c\alpha^n$. And if $\bar x\not\in C$, then our condition $\|z'\|\le\beta\max\{\|y\|,\|z\|\}$ implies that $|\lambda|\le\beta$. Thus, if $|\lambda|>\beta$, then $|\lambda|\ge\alpha$ and $\bar x\in\CC$. Assume from now on that $|\lambda|\ge\alpha$. Then $\bar x\in\CC$, and in particular, $\bar y\not=0$. Replacing $A$ by $-A$, if necessary, we may assume that $A\bar y\in c\bar y+Z$ with $c>0$. Denote by $\CC^{\pm}$ the two cones whose union is $\CC$, with $\CC^{+}$ being the one containing $\bar y$. Clearly, $\CC^{+}$ is invariant under $A$. This implies e.g.~that $\lambda$ is real and positive. Notice that $\CC^{+}$ has a non-empty interior. Thus, by the Krein-Rutman theorem, $\rho(A)$ is a simple eigenvalue of $A$. Furthermore, $A$ is strongly positive: $\CC^{+}\setminus\{0\}$ is mapped into the interior of $\CC^{+}$, since $\|z'\|\le\beta\alpha^{-1}\|y'\|$ whenever $y+z$ belongs to $\CC^{+}$. This guarantees [\rD, Theorem 1.2] that $\rho(A)$ is the only eigenvalue of $A$ that has an eigenvector in $\CC^{+}$. Consequently, our eigenvalue $\lambda$ is simple and equal to $\rho(A)$. This concludes the proof of \clm(eig). \qed \claim Definition(cones) Let $X=\YY\oplus\ZZ$, and let $\alpha>\beta$ be positive real numbers. Given two sections $\nu_1+X_1=\psi_1(X)$ and $\nu_2+X_2=\psi_2(X)$ of $\XX$, and a linear map $B: X_1\to X_2\,$, we say that $B$ satisfies the $(\alpha,\beta)$ cone condition, if $A=D\psi_2^{-1} B D\psi_1$ satisfies the hypotheses of \clm(eig). Consider again the Poincar\'e maps $P_j: S_{j-1}\to S_j$ described in Section 2.2. Denote by $u_j$ the intersection of our periodic orbit with the Poincar\'e plane $S_j$. \claim Corollary(eig2) If for each $j$, the derivative $DP_j(u_j)$ satisfies an $(\alpha_j,\beta_j)$ cone condition, then $D\Poinc(u_0)$ has a simple eigenvalue $\mu_1\ge\prod_j\alpha_j$ and no other spectrum outside the disk $|\mu|\le\prod_j\beta_j\,$. As far as the proof of \clm(Main) is concerned, our task is now reduced to verifying the hypotheses of \clm(fpt2), and of \clm(eig2), with $\beta_j<1<\alpha_j$ for all $j$. \section Functional setting %%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection The integral operator %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% It is convenient to rewrite the integral equation \equ(KStypeFour) as a fixed point problem $K_\nu(w)=w$ for the function $w(t)=u(t)-e^{tL}\nu$. The operator $K_\nu$ can be written as $K_\nu=\Lambda\circ\Gamma_\nu\,$, where $$ (\Lambda w)(t)=\int_{0}^t e^{(t-s)L}Mw(s)ds\,,\quad \bigl(\Gamma_\nu(w)\bigr)(t)= M^{-1}G\bigl(w+e^{tL}\nu\bigr)(t)\,, \equation(KKOneTwo) $$ for $0\le t\le T$. Here, $M$ is some invertible linear operator on $\XX$ that we are free to choose later. The problem with estimating $K_\nu$ on a computer is that the function $t\mapsto e^{tL}\nu$, and thus the integrand in $\Lambda$, can vary very rapidly near $t=0$. Such functions have to be considered e.g.~when estimating the derivative of the flow. We deal with this problem by partitioning $J=[0,T]$ into $n$ subintervals $J_i=[t_{i-1},t_i]$, with the partition being much finer near $t_0=0$, than near $t_n=T$, and controlling our functions on each subinterval $J_i$ separately. Define $\XX_\ssT$ to be space of all continuous functions $u:J\to\XX$ with a finite norm $$ \|u\|=\max_i\sum_{k=1}^\infty\sup_{t\in J_i}\|u_k(t)\bmv_k\|\,,\qquad u(t)=\sum_{k=1}^\infty u_k(t)\bmv_k\,. \equation(unorm) $$ We note that this norm depends on the partition $\{J_i\}$ of $J$. But the norms associated with two different partitions are equivalent. Our only reason for subdividing $J$ is to get more accurate estimates on the computer. For the results in this section, it suffices to consider just the trivial partition $\{J\}$. We recall that the functions $\bmv_k$ are assumed to be eigenvectors of $L$, with eigenvalues $-\lambda_k$ that tend to $-\infty$ as $k\to\infty$. In order to avoid growing factors $e^{-\lambda_k t}$ in the equation \equ(KStypeFive), we assume from now on that $\lambda_k\ge 0$ for all $k$. This represents no loss of generality, since a positive part of $L$ can always be incorporated into the nonlinear part $G$ of the vector field $L+G$. \claim Lemma(CompactOne) Let $0m}\lambda_k^{b-1}<\infty$, for some $m>0$. Then $\Lambda$ is compact on $\XX_\ssT\,$, and $\|\Lambda\|\le c(T+T^{b-a})$, for some constant $c$ that is independent of $T$. \proof Let $w\in\XX$ and $\wt w=\Lambda w$. Let $k\ge 1$. If $\lambda_k<1$, then $|\wt w_k(t)|\le 2t\|w_k\|$, where $\|w_k\|=\sup_{t\in J}|w_k(t)|$. If $\lambda_k\ge 1$ then $$ \eqalign{ \bigl|\wt w_k(t)\bigr| &\le\int_0^t e^{-\lambda_k(t-s)} (1+\lambda_k)^a|w_k(s)|\,ds\cr &\le 2\lambda_k^{b-1}t^{b-a} \bigl[(\lambda_kt)^{a-b}\bigl(1-e^{-\lambda_k t}\bigr)\bigr]\|w_k\|.\cr} \equation(CompactOne) $$ The expression $[\cdots]$ in this equation is bounded, uniformly in $k$ and $t$. Multiplying both sides of \equ(CompactOne) by $\|\bmv_k\|$, and summing over $k$, yields $\|\wt w\|\le c(T+T^{b-a})\|w\|$, with $c$ independent of $w$ and $T$. Denote by $\proj_k$ the canonical projection onto the one-dimensional subspace spanned by $\bmv_k\,$. Then $\Lambda\proj_k$ is compact, by Arzel\`a-Ascoli. The sum $\sum_k\Lambda\proj_k$ converges in norm to $\Lambda$, due to the factor $\lambda_k^{b-1}$ in \equ(CompactOne). Thus, $\Lambda$ is compact. \qed What remains to be proved is that $\Gamma_\nu$ is continuous and bounded on some appropriate domain in $\XX_\ssT\,$. Then $K_\nu=\Lambda\circ\Gamma_\nu$ is compact. Now it suffices to find a closed and convex set $C$ in this domain, such that $K_\nu(C)\subset C$. Then $K_\nu$ has a fixed point in $C$. On the computer, we determine such a set $C$ by starting with a singleton $C_0=\{\bar w\}$, where $\bar w$ is an approximate fixed point of $K_\nu\,$. Using a suitable enlargement map $C\mapsto C'$ for sets, we compute for $n=1,2,\ldots$ an enclosure $C_n$ for $K_\nu(C_{n-1}')$, until $C_n\subset C_{n-1}'$. The set $C=K(C_n)$ for the final value of $n$ is a bound on the fixed point $w$ of $K_\nu\,$, in the sense that $C\ni w$. This in turn yields a bound on $u(t)$ for $t\in J$, and a bound (in a sense that will be made more precise later) on the time-$t$ map $\nu\mapsto u(t)$. How exactly these bounds are implemented depends on the specific equation. In the remaining part of this paper, we describe the details for the Kuramoto-Sivashinski equation. \subsection The Kuramoto-Sivashinski equation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The one-dimensional Kuramoto-Sivashinski (KS) equation can be written as $$ \partial_t u=\LKS u-\alpha\partial_x(u^2)\,,\qquad \LKS=-4\partial_x^4-\alpha\partial_x^2\,. \equation(KSLLQ) $$ As mentioned earlier, we consider this equation for $\alpha=150$. But for now, $\alpha$ can be any positive real number. The boundary conditions considered are $u(t,0)=u(t,\pi)=0$, so the eigenvectors of $\LKS$ are given by $\bmv_k(x)=\sin(kx)$, where $k$ ranges over the set of all positive integers $\natural$. The corresponding eigenvalues are $\alpha k^2-4k^4$. As indicated earlier, we extract a negative part $L$ from $\LKS$. To this end, let $\kappa\ge\sqrt{\alpha}/2$, so that $\alpha k^2-4k^4\le 0$ for $k\ge\kappa$. Then define $L$ and $L'$ by the equations $L\bmv_k=-\lambda_k\bmv_k$ and $L'\bmv_k=-\lambda'_k\bmv_k$, respectively, where $$ \lambda_k=\cases{ 0, &if $k\le\kappa$;\cr 4k^4-\alpha k^2 &if $k>\kappa$;\cr}\qquad \lambda'_k=\cases{4k^4-\alpha k^2 &if $k\le\kappa$;\cr 0 &if $k>\kappa$;\cr} \equation(lambdak) $$ Clearly, $\LKS=L+L'$, and $L$ has no positive eigenvalues. The KS equation \equ(KSLLQ) can now be written in the standard form \equ(KStypeOne), $$ \partial_t u=L u+G(u)\,,\qquad G(u)=L'u-\alpha\partial_x(u^2)\,. \equation(KSLG) $$ At this point, we need to define some function spaces. Let $\rho$ be a fixed positive real number. In addition to $\bmv_k(x)=\sin(kx)$ for integers $k>0$, we also consider $\bmv_k(x)=\cos(kx)$ for $k\le 0$. Given a real number $p>0$, and a non-empty set of integers $\KK$, define $\AA_p^\ssKK$ to be the completion of ${\rm Span}\bigl(\{\bmv_k\}_{k\in\KK}\bigr)$ with respect to the norm $$ \|f\|_p=\sum_{k\in\KK}|f_k|[k]^p e^{\rho|k|}\,,\qquad f=\sum_{k\in\KK} f_k\bmv_k\,, \equation(Fourier) $$ where $[k]=\max(|k|,1)$. Notice that the functions in $\AA_p^\ssKK$ have analytic and bounded extensions to the strip $|{\rm Im}(x)|<\rho$. The space $\XX$ referred to in earlier sections is $\AA_p^\ssnatural$. For now, $p>0$ is arbitrary; but later on, we will choose $p=0$. A slightly different (but equivalent) norm on $\XX$ is used in our definition of the boxes $B_j\,$, as will be described later. The space of continuous curves $u:J\to\AA_p^\ssKK$ with a finite norm $$ \|u\|_p=\max_i\sum_{k\in\KK}[k]^pe^{\rho|k|}\sup_{t\in J_i}|u_k(t)|\,, \qquad u(t)=\sum_{k\in\KK}u_k(t)\bmv_k\,, \equation(unorm) $$ will be denoted by $\CC(J,\AA_p^\ssKK)$. In particular, $\CC(J,\XX)$ agrees with the space $\XX_\ssT$ defined in Subsection 3.1. A useful property of the spaces $\AA_p^\ssinteger$ and $\CC(J,\AA_p^\ssinteger)$ is that they are both Banach algebras. As described in the previous subsection, we solve \equ(KSLG) via the fixed point equation $K_\nu(w)=w$ for $w(t)=u(t)-e^{tL}\nu$, where $K_\nu=\Lambda\circ\Gamma_\nu\,$, with $\Gamma_\nu$ and $\Lambda$ as defined by equation \equ(KKOneTwo). Notice that this map $K_\nu$ is independent of the choice of the operator $M$. \claim Theorem(Compact) $K_\nu$ is a compact map on $\XX_\ssT\,$, for each $\nu\in X$. If $B\subset\XX$ is bounded and non-empty, and if $C$ is a closed convex subset of $\XX_\ssT\,$, such that $K_\nu(C)\subset C$, for every $\nu\in B$, then $K_\nu$ has a unique fixed point $w\in C$, for every $\nu\in B$. If $B$ is open, then the map $\nu\mapsto w$ is of class $C^1$ on $B$. \proof Let $a={1\over 3}$ and $b={2\over 3}$. Then the hypothesis of \clm(CompactOne) is satisfied, implying that $\Lambda$ is compact. Furthermore, since $\CC(J,\AA_p^\ssinteger)$ is a Banach algebra, the map $u\mapsto u^2$ is of class $C^2$ on all of $\AA_p^\ssinteger\,$. Clearly, the same holds for $\Gamma_\nu\,$. Thus, $K_\nu$ is compact, and the existence of a fixed point follows from Schauder's fixed point theorem. Let $w_1$ and $w_2$ be two such fixed points. Assume for contradiction that $w_1\not=w_2\,$, and let $T_0=\inf\{t\in[0,T]: w_1(t)\not=w_2(t)\}$. Replacing $w_i$ by $t\mapsto w_i(T_0+t)-e^{tL}w_i(T_0)$, if necessary, we can assume that $T_0=0$. In what follows, a curve or operator associated with a time interval $[0,s]$ will be given a subscript $s$. Let $r>0$. By \clm(CompactOne), $K_{\nu,s}$ is a contraction on the ball $\|w_s\|_p0$ is sufficiently small. By continuity, both $w_{1,s}$ and $w_{2,s}$ belong to this ball, if $s>0$ has been chosen sufficiently small. As a result, $w_{1,s}=w_{2,s}\,$, contradicting the assumption that $w_1\not=w_2\,$. Let $v$ be an eigenvector of $DK_\nu(w_1)$, for some eigenvalue $\lambda$, and define $T_0=\inf\{t\in[0,T]: v(t)\not=0\}$. After translating $w_1$ and $v$ in time by $T_0\,$, if necessary, we can assume that $T_0=0$. Then $v_s$ is an eigenvector of $DK_{\nu,s}(w_{1,s})$, with eigenvalue $\lambda$; and by taking $s\downarrow 0$, we see that $\lambda=0$. In particular, $DK_\nu(w_1)$ has no eigenvalue $1$. Thus, by the implicit function theorem, the map $\nu\mapsto w_1$ is of class $C^1$. \qed Consider now a section $S=\eta^{-1}(s)$, defined by some nonzero continuous functional $\eta:\XX\to\real$, and some $s\in\real$. Let $B$ be a non-empty bounded set in $\XX$. In what follows, differentiability of a function on $B$ means differentiability in an open neighborhood of $B$. \claim Theorem(KSPoinc) Let $00$. If the section $S$ is transversal to the flow, then the corresponding Poincar\'e map $P: B\to S$ is well defined, of class $C^1$, and compact. \proof We may assume that $B$ is open. Let $00$. The same holds for the map $u(0)\mapsto\dot u(t)$ as well, since $L+G$ is a smooth map from $\AA_{r+4}^\ssnatural$ to $\AA_r^\ssnatural\,$, for any $r>0$, This in turn implies that the flow $\Flow: (t,\nu)\mapsto\Flow_t(\nu)$ is of class $C^1$ on $[a,c]\times B$. Assume now that $S$ is transversal to this flow, in the sense of \clm(transversal). Then, by the implicit function theorem, the equation $\eta(\Flow_t(\nu))=s$ has a unique solution $t=t(\nu)$, and this crossing time is a $C^1$ function on $B$. Composing $\nu\mapsto(t(\nu),\nu)$ with $\Flow$ yields the Poincar\'e map $P: B\to S$, and this map is $C^1$ by the chain rule. \qed \medskip\noindent {\bf Convention.} {}From now on, we only consider $p=0$ and drop the index $p$. \bigskip The remaining part of the paper is devoted to the proof of the following theorem, which, together with \clm(fpt2) and \clm(eig2), implies \clm(Main). \claim Theorem(boxes) For every integer $j$, modulo $M=4294$, there exists a section $S_j\subset\AA^\ssnatural$, a box $B_j\subset S_j\,$, a time interval $[a_j,c_j]$, and two positive real numbers $\beta_j<1<\alpha_j\,$, such that the following holds. For each $j$, the flow $\Phi: [a_j,c_j]\times B_{j-1}\to\AA^\ssnatural$ is transversal to the section $S_j\,$, and the box $B_{j-1}$ $P_j$-covers $B_j\,$. If $j\mapsto u_j\in B_j$ satisfies $P_j(u_{j-1})=u_j\,$, for each $j$, then the derivative $DP_j(u_{j-1})$ satisfies the $(\alpha_j,\beta_j)$ cone condition, for each $j$. Furthermore, $\prod_j\alpha_j\ge4.8$ and $\prod_j\beta_j\le0.69$. \section Implementation and further details %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection Integration %%%%%%%%%%%%%%%%%%%%%%% In order to obtain reasonably accurate error bounds for the integral operator $K_\nu\,$, we decompose this operator into several parts and estimate each separately. In a first step, we write $K_\nu(w)=P(\nu,w)+Q(\nu,w)$, where $P$ is linear and $Q$ bilinear. Then $Q(\nu,w)$ is split into three terms $Q^{(n)}(\nu,w)$ that are homogeneous of degree $n=0,1,2$ in $w$. After substituting the sine-series for $\nu$ and $w$, we end up with integrals like $$ \bigl(Q^{(1+)}_m(\nu,w)\bigr)(t) =-\alpha m\sum_{k+\ell=m}\nu_k \int_0^te^{-\lambda_m(t-s)}e^{-\lambda_k s} w_\ell(s)\,ds\,. \equation(QOnePlus) $$ To be more precise, this term is the first of two contributions to the $m$-th Fourier coefficient of $Q^{(1)}(\nu,w)$. The two contributions correspond to the two terms in the identity $ \partial_x\bigl[2\sin(kx)\sin(\ell x)\bigr] =(k+\ell)\sin\bigl((k+\ell)x\bigr) -|k-\ell|\sin\bigl(|k-\ell|x\bigr)\,. $ The integral in \equ(QOnePlus) can be computed explicitly if $w_\ell$ is a polynomial. For other terms, we use the following estimate. Define $\|f\|_i=\sup_{t\in J_i}|f(t)|$ and $$ G_i(k,\ell)= {k+\ell\over(\lambda_{k+\ell}-\lambda_k)+2/t_i}\,. \equation(Gj) $$ \claim Proposition(QOnePlusBound) Let $\KK$ and $\LL$ be the supports of $k\mapsto\nu_k$ and $\ell\mapsto w_\ell\,$, respectively. Then $$ \bigl\|Q^{(1+)}(\nu,w)\bigr\|_i \le 2\alpha\|\nu\| \|w\| \sup_{k\in\KK\atop\ell\in\LL} G_i(k,\ell)e^{-\lambda_k t_{i-1}}\,. \equation(QOnePlusBound) $$ The supremum in equation \equ(QOnePlusBound) can be determined in a finite computation, using the following monotonicity properties of $G_i\,$. \claim Proposition(Fpj) For $\ell>0$, the set of all $k>\kappa$ such that $G_i(k+1,\ell)(\alpha/12)^{1/2}$. An analogous statement holds with the roles of $k$ and $\ell$ exchanged. Furthermore, $G_i(k,\ell+1)\le G_i(k+1,\ell)$ for all $k$ and $\ell$. Similar bounds and monotonicity properties can be obtained for the remaining terms in the splitting of $K_\nu(\omega)$. For details we refer to the package {\tt ContFuns.CE.Ops.KS} of computer programs [\rFiles]. The proofs of these propositions are elementary and thus will not be given here. \subsection Choice of boxes %%%%%%%%%%%%%%%%%%%%%%%%%%% Our boxes $B_j$ are centered at points $\bar u_j=\bar u(j\bar\tau/M)$ along an approximate periodic orbit $\bar u$, where $0\le j Interval}), or in purely numeric mode ({\tt Scalar => Numeric}) if the goal is to find an approximate solution. The other levels merely organize the proof. Many of these steps require accurate bounds to succeed, and this has to be achieved with a finite (and reasonable) number of operations. This is made possible by the fact that the map $K_\nu$ is uniformly approximable by finite dimensional mappings. It allows for accurate bounds that involve only finitely many inequalities. The general approach is quite standard by now. We start by associating to a space $X$ a collection $\std(X)$ of subsets of $X$ that are representable on the computer. We will refer to these sets as ``standard sets'' for $X$. A ``bound'' on an element $w\in X$ is then a set $W\in\std(X)$ containing $w$, while a bound on a map $f: X\to Y$ is a map $F: D_\ssF\to\std(Y)$, with domain $D_\ssF\subset\std(X)$, such that $f(w)\in F(W)$ whenever $w\in W\in D_\ssF\,$. Notice that the composition of two bounds, if defined, is a bound on the corresponding composed map. This and other properties allow us to combine bounds on elementary maps into bounds on more complex maps like $K_\nu\,$, and thus to mechanize the necessary estimates. Bounds are implemented as procedure or functions in our programs. Any procedure (or function) that uses a theorem first tries to verify that the hypotheses of the theorem are satisfied, for the given input. If the hypotheses cannot be verified, then the procedure aborts with an {\tt Error} message. In that sense, every implemented bound $F$ knows its domain: If a procedure (and thus any other procedure that may get invoked in the process) terminates without generating an {\tt Error}, then the input is by definition in the domain of $F$. The basic bounds used in the present proof have been developed already in [\rAKT], up to the level of bounds on basic operations (like sums, products, antiderivatives, norms, etc.) involving the spaces $\real$ and $\XX^\ssinteger$, as well as between products of these spaces. Thus, in order to avoid undue repetition, the reader is referred to [\rAKT,\rAK] for a description of the bounds used at this level. Here, we also have to choose and represent appropriate sets in the space $\CC(J,\XX^\ssinteger)$. For functions in $C(J,\real)$, we use approximating polynomials of degrees up to $m=20$, and error estimates on $n=10$ subintervals $J_i\,$. Given $G=(G_0,\dots,G_m)$ in $\std(\real)^{m+1}$ and $H=(H_1,\dots,H_n)$ in $\std(\real_+)^n$, define $C_{\ssG,\ssH}$ to be the set of all functions $f\in C(J,\real)$ that admit a representation $$ f(t)=\sum_{k=0}^m g_k t^k+h(t)\,,\qquad h\in C(J,\real)\,, \equation(ContFun) $$ such that $g_j\in G_j$ for all $j$, and $\|h\|_i\le h_i\in H_i$ for all $i$. We now define $\std(C(J,\real))$ to be the collection of all such sets $C_{\ssG,\ssH}\,$. These standard sets correspond to the data type {\tt ContFun} in our programs. Consider now the space $\CC(J,\AA^\ssinteger)$. Functions in this space can be represented as Fourier series $u(t)=\sum_k u_k(t)\bmv_k$ with coefficients $u_k\in C(J,\real)$. The data type for function $\nu=\sum_k\nu_k\bmv_k$ in $\AA^\ssinteger$, and the corresponding collection of subsets $\std(\AA^\ssinteger)$, have already been defined in [\rAK]. In fact, this type was derived from a generic data type {\tt Fourier}, with coefficients in some unspecified Banach algebra, whose standard sets are represented by a generic type {\tt FCoeff}. We can take advantage of this by instantiating {\tt FCoeff} with {\tt ContFun}, to define a derived type {\tt TFourier}. The sets associated with data of type {\tt TFourier} are our standard sets for the space $\CC(J,\AA^\ssinteger)$. We note that the (bound on the) norm inherited from this procedure corresponds to the trivial partition $\{J\}$ of $J$. The norm for other choices of the partition has to be implemented afterwards. It is now straightforward to implement bounds on the basic operations involving the spaces $\AA^\ssinteger$ and $\CC(J,\AA^\ssinteger)$. This includes e.g.~the evaluation map $u\mapsto u(t)$ from $\CC(J,\AA^\ssinteger)$ to $\AA^\ssinteger$. A bound on the map $K_\rho$ is straightforward as well, albeit tedious, as Subsection 4.1 indicates. Our bound on $K_\nu$ yields a bound on the time-$t$ map $\Flow_t\,$, as described earlier. The map whose fixed point solves \equ(KSvar) is very similar to $K_\nu\,$, and we can use the exact same estimates as for $K_\nu\,$. This in turn yields a abound on the derivative $D\Flow_t\,$. For the intermediate Poincar\'e maps $P_j$ we use two different bounds. Let us first describe the ``simple'' version and its application. We start with a numerical guess for a time-interval $[a,c]$ that should contain the crossing times $t(\nu)$, for all initial conditions $\nu\in B_j\,$. Then we verify the transversality condition in \clm(transversal), with $B=B_{j-1}$ and $S=S_j\,$, using the convexity argument described in Subsection 4.3, for both $f=\Flow_a$ and $f=\Flow_c\,$. A bound on $P_j$ is now given by a bound on $P_j'=\mean\Flow_t$ that is valid for every $t\in[a,c]$. Here, $\mean x$ is the vector obtained from $x\in\XX$ by setting its second coordinate (in the basis $\Sigma_j$) equal to zero. Consider now the problem of verifying that $B_{j-1}$ $P_j'$-covers $B_j\,$. Let $f=\psi_j^{-1}\circ P_j'\circ\psi_{j-1}\,$, where $\psi_{j-1}$ and $\psi_j$ are the affine maps associated with the boxes $B_{j-1}$ and $B_j\,$, respectively. That is, $B_j=\psi_j(B)$, where $B$ denotes the unit ball in the space $X=\YY\oplus\ZZ$, equipped with the norm \equ(newnorm), where $x_2=0$. Let $I=\{1,3,\ldots,20\}$. Denote by $\proj$ the canonical projection in $X$ onto the span of $\{\bmv_k\}_{k\in I}\,$. Then every $x\in X$ has a unique representation $x=\sum_{k\in I}c_k(x)\bmv_k+\xi(x)$, where $\xi(x)=(\Id-\proj)x$. Using the notation from Subsection 4.3, the box $B$ has $m=2^{19}$ corners $b+w_i\,$, with $c_k(w_i)=\pm 1$ and $\xi(w_i)=0$. We check that $c_1(f(b+w_i))\ge\alpha_j>1$ whenever $c_1(w_i)=1$, and that $c_1(f(b+w_i))\le-\alpha_j<-1$ whenever $c_1(w_i)=-1$. In addition, we verify that $|c_k(f(b+w_i))|\le\beta_j<1$ for $k\ge 3$, and that $\|\xi(f(b+w_i))\|\le\beta_j<1$. This is done by using a bound $F$ on $Df$, as described in Subsection 4.3. By convexity, the above inequalities imply that $B_{j-1}$ $P_j'$-covers $B_j\,$. This holds for every $t\in[a,c]$, so $B_{j-1}$ $P_j$-covers $B_j\,$. Once these covering relations have been verified, the existence of the periodic orbit $u$ follows from \clm(fpt2). This allows us to bound the derivatives $DP_j(u_{j-1})$ by using equation \equ(DerPmap) and \clm(EstVel). Now we repeat the steps described above, but with $F$ a bound on the derivative of $f=\psi_j^{-1}\circ P_j\circ\psi_{j-1}$ on $B$. By linearity, this is equivalent to verifying an $(\alpha_j,\beta_j)$ cone condition. For a detailed and complete description of all these steps, we refer to the source code (in Ada95) and input data for our computer programs [\rFiles]. These programs were run successfully on several different types of machines, using public versions of the GNAT compiler [\rGnat]). \references %%%%%%%%%%% {\ninepoint \item{[\rM]} C.~Miranda, {\it Un'osservazione su un teorema di Brouwer}, Boll.~Un.~Mat.~Ital. 3, no.~2, 5--7 (1940). \item{[\rCCP]} F.~Christiansen, P.~Cvitanovi\'c, V.~Putkaradze, {\it Spatiotemporal chaos in terms of unstable recurrent patterns}, Nonlinearity 10, 55-–70 (1997). \item{[\rKT]} Y.~Kuramoto, T.~Tsuzuki, {\it Persistent propagation of concentration waves in dissipative media far from thermal equilibrium}, Progr.~Theor.~Phys. 55, 365--369 (1976). \item{[\rS]} G.I.~Sivashinsky, {\it Nonlinear analysis of hydrodynamic instability in laminal flames - I. Derivation of basic equations}, Acta Astr. 4, 1177--1206 (1977). \item{[\rKNS]} J.G.~Kevrekidis, B.~Nicolaenko and J.C.~Scovel, {\it Back in the saddle again: a computer assisted study of the Kuramoto-Sivashinsky equation}, SIAM J.~Appl.~Math. 50, 760--790 (1990). \item{[\rJKT]} M.S.~Jolly, J.G.~Kevrekidis and E.S.~Titi, {\it Approximate inertial manifolds for the Kuramoto-Sivashinsky equation: analysis and computations}, Physica D 44, 38--60 (1990). \item{[\rIl]} Yu.S.~Ilyashenko, {\it Global analysis of the phase portrait for the Kuramoto-Sivashinski equation}, J.~Dyn.~Differ.~Equations 4, 585--615 (1992). \item{[\rCEES]} P.~Collet, J.-P.~Eckmann, H.~Epstein, J.~Stubbe, {\it A global attracting set for the Kuramoto-Sivashinsky equation}, Commun.~Math.~Phys. 152, 203--214 (1993). \item{[\rD]}Yihong Du, {\it Order structure and topological methods in nonlinear partial differential equations}, World Scientific (2006),\hfil\break {\tt www.worldscibooks.com/mathematics/5999.html} \item{[\rZM]} P.~Zgliczy\'{n}ski, K.~Mischaikow, {\it Rigorous numerics for partial differential equations: The Kuramoto-Sivashinsky equation}, Found.~of Comp.~Math. 1, 255--288 (2001). \item{[\rZMb]} P.~Zgliczy\'{n}ski, K.~Mischaikow, {\it Towards a rigorous steady states bifurcation diagram for the Kuramoto-Sivashinsky equation - a computer assisted rigorous approach}, \item{[\rZ]} P.~Zgliczy\'{n}ski {\it Rigorous Numerics for Dissipative PDEs III. An effective algorithm for rigorous integration of dissipative PDEs}, preprint 2008. \item{[\rAZ]} G.~Arioli and P.~Zgliczy\'{n}ski, {\it Symbolic dynamics for the H\'enon-Heiles Hamiltonian on the critical energy level}, J.~Diff.~Eq 171, 173--202 (2001). \item{[\rZG]} P.~Zgliczy\'{n}ski, M.~Gidea {\it Covering relations for multidimensional dynamical systems} J.~Differential Equations 202, 1, 32--58 (2004). \item{[\rGZ]} M.~Gidea, P.~Zgliczy\'{n}ski {\it Covering relations for multidimensional dynamical systems. II.} J.~Differential Equations 202, 1, 59--80 (2004). \item{[\rAKT]}G.~Arioli, H.~Koch, S.~Terracini, {\it Two novel methods and multi-mode periodic solutions for the Fermi-Pasta-Ulam model}, Comm.~Math.~Phys. 255, 1--19 (2005). \item{[\rAK]} G.~Arioli, H.~Koch {\it Computer-assisted methods for the study of stationary solutions in dissipative systems, applied to the Kuramoto-Sivashinski equation}. \item{[\rDS]} N.~Dunford, J.T.~Schwartz, {\it Linear Operators, Part I: General Theory}, Wiley--Interscience, New Edition (1988). \item{[\rPazy]} A.~Pazy, {\it Semigroups of Linear Operators and Applications to Partial Differential Equations}, Springer Verlag New York (1983). %%%%%%%% computation \item{[\rIEEE]} The Institute of Electrical and Electronics Engineers, Inc., {\it IEEE Standard for Binary Float\-ing--Point Arithmetic,} ANSI/IEEE Std 754--1985. \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 1246 (1997). See also {\tt http://www.adahome.com/rm95/}. \item{[\rFiles]} Ada files and data are included with the preprint {\tt mp\_arc 10--9}. \item{[\rGnat]} The GNU NYU Ada 9X Translator, available at {\tt ftp://cs.nyu.edu/pub/gnat} and many other places. } \bye