Rigorously Verified Computing for Infinite Dimensional Nonlinear Dynamics (14w5098)

Arriving in Banff, Alberta Sunday, September 21 and departing Friday September 26, 2014


(Université Laval)

(Rutgers University, USA)

(Hamburg University of Technology)

(Vrije Universiteit Amsterdam)

JF Williams (Simon Fraser University)


Partial differential equations are at the core of the mathematical description of the world around us: from Schr"odinger's equation in quantum mechanics to the Navier-Stokes equations in fluid dynamics, from the reaction-diffusion equations governing biochemistry to the Black-Scholes equation in mathematical finance.The nonlinear nature of many of these equations makes their analysis challenging. Two complementary approaches are used to investigate such problems. On the one hand, one can exploit geometric and topological ideas to perform a global analysis. This provides robust qualitative information. Ideally this is coupled with numerical calculations, which offer detailed quantitative information and clear pictures of the solutions, but the information from the numerics is local (in parameter space) and non-rigorous.Dramatic advances in algorithms, analysis, code, and computer speed and memory have opened the possibility of utilizing the power and robustness of topological and analytic methods to rigorously verify computational results. Computer assisted proofs of the existence of low dimensional dynamical structures, e.g. fixed points, periodic orbits, heteroclinic and homoclinic orbits, can be used as building blocks in global analysis, either using gluing methods from dynamical systems theory or via Morse-Conley-Floer theory. In this way local, rigorously verified, numerical solutions form the seeds of information from which additional global understanding can be gained.The method of rigorous verified computing, developed in the past decade, has primarily been applied to a range of ordinary differential equations and maps (e.g.~cite{BHMP,LM,T,BL,WZ} to name just a few) and one-variable periodic patterns in PDEs and delay equations~cite{ZM,L}. Additionally, several multi-dimensional PDE problems have been studied, e.g. in the area of elliptic PDEs~cite{YN,WN,P} and in settings with periodic boundary conditions~cite{GL}. Furthermore, eigenvalue problems have been considered~cite{BMZ,WPN}, parameter continuation has been implemented~cite{BLM}, and parametrization methods for invariant manifolds enable the study of connecting orbits in ODEs~cite{BJLM}. Also, rigorously verified computations were combined with Morse-Conley theory to study global dynamics of gradient PDEs~cite{DHMO}. Two recent breakthroughs promise to accelerate developments in the field. First, the use Chebyshev polynomials to attack connecting orbit problems, which greatly increases the computational efficiency. Second, the application of these techniques in the setting of spatio-temporal periodicity in parabolic PDEs.We thus stand at the start of the emerging field of computer assisted proofs for infinite dimensional nonlinear dynamics generated by PDEs, integral equations, delay equations, as well as infinite dimensional maps.Rigorous verification goes far beyond an a posteriori analysis of numerical computations. In a nutshell, verification methods are mathematical theorems formulated in such a way that the assumptions can be rigorously verified on a computer. Indeed, it requires an a priori setup that allows analysis and numerics to go hand in hand: the choice of function spaces, the choice of the basis functions/elements and Galerkin projections, the analytic estimates, and the computational parameters must all work together to bound the errors due to approximation, rounding and truncation sufficiently tightly for the verification proof to go through. On top of that, for high and infinite dimensional problems additional aspects arise. On the analysis side, we need to deal with much subtler and more involved truncation estimates and, for connecting orbits, with high or infinite dimensional invariant manifolds. On the algorithm side, we must find suitable pre-conditioners and develop efficient interval-arithmetic based algorithms. Finally we need to understand how to tie these computational results to the geometric and topological ideas of global nonlinear analysis that form the framework for our understanding of nonlinear dynamics.This leads us to the following questions, which will be central to the workshop:
    item Where do our current algorithms fail and how can we improve them to suit the rigorously verified computing approach for a wide variety of nonlinear PDE problems? item Which are the ingredients from scientific computing, numerical linear algebra and related interval arithmetic methods, that are needed for large scale PDE problems? item Which types of PDE problems can be solved with rigorously verified computing in the near future? For which types is there not much hope at present, and why not? Which tools are missing?
To answer these questions we plan to bring together experts in scientific computing, numerical analysis with result verification, applied PDE analysis, and nonlinear dynamical systems. The aim of the workshop is to foster collaboration in order to develop a flexible analytic strategy tied with corresponding fast and robust algorithms.As indicated above, rigorously verified computations require a variety of technical tools ranging from specific estimates to theorems in dynamics to specialized algorithms. To spur parallel progress in this direction we will identify a select set of challenging infinite dimensional problems around which the group can focus its efforts.A few examples of the type of challenges that we strive for are:
    item Connecting orbits in ill-posed (strongly indefinite) infinite dimensional dynamical systems. In Floer homology theory the transversal connecting orbits form the basis for the boundary operator. Computing such connecting orbits for e.g. nonlinear Cauchy-Riemann equations thus gives seeds of topological dynamic information. Similar connecting orbit problems appear in a patterns formation context, namely in the description of spiral waves and periodically modulated traveling waves. item Turbulence in fluid flows may be related to chaotic dynamics in the 3D Navier-Stokes equations. One way to approach this is by locating (rigorously) a periodic fluid motion in a convection cell, and subsequently proving the existence of an orbit that is homoclinic to this cycle. Via a forcing result from dynamical systems theory this implies that the fluid motion must then be chaotic/turbulent. item The hot spots conjecture, which can be formulated as follows: the second Neumann eigenfunction attains its extrema only at the boundary of the domain. The polymath project~cite{polymath} now focuses on a rigorously verified numerical strategy to solve the hot spots conjecture for all acute angle triangles. This nicely illustrates the timeliness of the workshop.
begin{thebibliography}{99} bibitem{polymath} Polymath7: the Hot Spots Conjecture; http://polymathprojects.org/2012/09/10/polymath7-research-threads-4-the-hot-spots-conjecture/. bibitem{BHMP} B.~Breuer, J.~Hor{'a}k, P.~J. McKenna, and M.~Plum. newblock A computer-assisted existence and multiplicity proof for travelling waves in a nonlinearly supported beam. newblock {em J. Differential Equations}, 224(1):60--97, 2006. bibitem{BMZ} B.~M. Brown, D.~K.~R. McCormack, and A.~Zettl. newblock On a computer assisted proof of the existence of eigenvalues below the essential spectrum of the {S}turm-{L}iouville problem. newblock {em J. Comput. Appl. Math.}, 125(1-2):385--393, 2000. newblock Numerical analysis 2000, Vol. VI, Ordinary differential equations and integral equations. bibitem{DHMO} Sarah Day, Yasuaki Hiraoka, Konstantin Mischaikow, and Toshiyuki Ogawa. newblock Rigorous numerics for global dynamics: a study of the {S}wift-{H}ohenberg equation. newblock {em SIAM J. Appl. Dyn. Syst.}, 4(1):1--31 (electronic), 2005. bibitem{GL} Marcio Gameiro and Jean-Philippe Lessard. newblock Rigorous computation of smooth branches of equilibria for the three dimensional {C}ahn-{H}illiard equation. newblock {em Numer. Math.}, 117(4):753--778, 2011. bibitem{LAN} Oscar~E. Lanford, III. newblock A computer-assisted proof of the {F}eigenbaum conjectures. newblock {em Bull. Amer. Math. Soc. (N.S.)}, 6(3):427--434, 1982. bibitem{L} Jean-Philippe Lessard. newblock Recent advances about the uniqueness of the slowly oscillating periodic solutions of {W}right's equation. newblock {em J. Differential Equations}, 248(5):992--1016, 2010. bibitem{LM} H{'e}ctor~E. Lomel{'{i}} and James~D. Meiss. newblock Quadratic volume-preserving maps. newblock {em Nonlinearity}, 11(3):557--574, 1998. bibitem{P} Michael Plum. newblock Computer-assisted proofs for semilinear elliptic boundary value problems. newblock {em Japan J. Indust. Appl. Math.}, 26(2-3):419--442, 2009. bibitem{T} Warwick Tucker. newblock A rigorous {ODE} solver and {S}male's 14th problem. newblock {em Found. Comput. Math.}, 2(1):53--117, 2002. bibitem{BL} Jan~Bouwe van~den Berg and Jean-Philippe Lessard. newblock Chaotic braided solutions via rigorous numerics: chaos in the {S}wift-{H}ohenberg equation. newblock {em SIAM J. Appl. Dyn. Syst.}, 7(3):988--1031, 2008. bibitem{BLM} Jan~Bouwe van~den Berg, Jean-Philippe Lessard, and Konstantin Mischaikow. newblock Global smooth solution curves using rigorous branch following. newblock {em Math. Comp.}, 79(271):1565--1584, 2010. bibitem{BJLM} Jan~Bouwe van~den Berg, Jason~D. Mireles-James, Jean-Philippe Lessard, and Konstantin Mischaikow. newblock Rigorous numerics for symmetric connecting orbits: even homoclinics of the {G}ray-{S}cott equation. newblock {em SIAM J. Math. Anal.}, 43(4):1557--1594, 2011. bibitem{WN} Yoshitaka Watanabe and Mitsuhiro~T. Nakao. newblock Numerical verifications of solutions for nonlinear elliptic equations. newblock {em Japan J. Indust. Appl. Math.}, 10(1):165--178, 1993. bibitem{WPN} Yoshitaka Watanabe, Michael Plum, and Mitsuhiro~T. Nakao. newblock A computer-assisted instability proof for the {O}rr-{S}ommerfeld problem with {P}oiseuille flow. newblock {em ZAMM Z. Angew. Math. Mech.}, 89(1):5--18, 2009. bibitem{WZ} Daniel Wilczak and Piotr Zgliczynski. newblock Heteroclinic connections between periodic orbits in planar restricted circular three-body problem---a computer assisted proof. newblock {em Comm. Math. Phys.}, 234(1):37--75, 2003. bibitem{YN} Nobito Yamamoto and Mitsuhiro~T. Nakao. newblock Numerical verifications for solutions to elliptic equations using residual iterations with a higher order finite element. newblock {em J. Comput. Appl. Math.}, 60(1-2):271--279, 1995. newblock Linear/nonlinear iterative methods and verification of solution (Matsuyama, 1993). bibitem{ZM} Piotr Zgliczy{'n}ski and Konstantin Mischaikow. newblock Rigorous numerics for partial differential equations: the {K}uramoto-{S}ivashinsky equation. newblock {em Found. Comput. Math.}, 1(3):255--288, 2001. end{thebibliography}