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

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

## Organizers

Jean-Philippe Lessard (Université Laval)

Konstantin Mischaikow (Rutgers University, USA)

Siegfried Rump (Hamburg University of Technology)

Jan Bouwe van den Berg (Vrije Universiteit Amsterdam)

JF Williams (Simon Fraser University)

## Objectives

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?

- 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.