11-15 July 2011

SciCADE 2011

hosted by the Fields Institute,
held at the University of Toronto

New Talent Award

Sign up for E-lerts programs(PUT_AT_SIGN_HERE)fields.utoronto.ca

Contact Us gensci(PUT_AT_SIGN_HERE)fields.utoronto.ca

Validated Integration Methods for ODEs, I
Organized by
Markus Neher, Karlsruhe Institute of Technology, Germany

Validated integration methods for ODEs aim at computing rigorous bounds for specific solutions of ODEs. Interval arithmetic has been used for almost 50 years for this purpose. Recently, Taylor model methods for ODEs have been developed by Berz and Makino by combining interval arithmetic with computer algebra. Taylor models reduce the dependency problem and the wrapping effect intrinsic to interval arithmetic. They also benefit from their capability of representing nonconvex sets, which is especially advantageous for enclosing the flows of nonlinear ODEs.

The talks in the minisymosium report on recent developments in validated methods for ODEs, including applications to practical problems.

Markus Neher,
Karlsruhe Institute of Technology,

Introduction to Validated Methods for ODEs
Validated integration methods for ODEs are methods that compute rigorous bounds for specific solutions of ODEs. In our talk, we compare interval methods with Taylor model methods, highlighting recent achievements and current challenges.
Martin Berz,
Michigan State University

Verified integration of flows for large ranges of initial conditions

We review Taylor-model based methods and the rigorous verified integrator COSY-VI for the verified integration of ODEs and flows. Particular emphasis is given to the suppression of the wrapping effect to very high accuracy while representing large ranges of initial conditions and parameters by automatic domain decomposition methods.

We discuss applications for computer assisted proofs of the study of the Lorenz system. We determine rigorous representations for the flow for a very large box of initial conditions containing all of the commonly studied dynamics. With rather moderate computational effort, the entire flow can be represented uniformly to an accuracy of less than 1E-6. The resulting flows can be used for the study of dynamics using discretizations and graph-based methods.

Kyoko Makino,
Michigan State University
Computer assisted proof of chaoticity of the Lorenz system for large ranges of parameters

The Lorenz system is one of the important showcases of dynamical systems. However, while the dynamics appears chaotic for large ranges of parameters, rigorous proofs of these conjectures have so far been possible only for isolated values of parameters. We study heuristically determined parameter dependent topological rectangles on a fixed surface that appear to lead to horseshoe crossings in the second return to the surface. Using the verified integrator COSY VI, the parameter dependent boundaries of the rectangles are transported to the second return and projected to the Poincare surfaces, and used for the verification of the Markov crossing property. Utilizing the continuity of the second return map, this allows to show chaoticity a range of rho from about 25 to 95.

* This is joint work with Alexander Wittig, Sheldon Newhouse and Yuting Zou

Alex Wittig,
Michigan State University

Sharp Verified High-Order Enclosures of Invariant Manifolds of ODEs

A method to construct very accurate polynomial approximations of invariant manifolds of hyperbolic critical points in sufficiently smooth autonomous ordinary differential equations is presented. This construction is performed using differential algebra methods and also works in resonant cases as well as in arbitrary dimensions.

The constructed polynomial manifold approximation is then outfit with a tight remainder bound (typically of size $10^{-12}$ or less), the correctness of which is verified using Taylor Model techniques. While the methods presented work in arbitrary dimension, special attention is given to the three dimensional case. The result is a very sharp, verified high-order enclosure of the local invariant manifolds. Using verified integration, these local manifold pieces can be integrated to obtain rigorous enclosures of large pieces of the invariant manifolds.

We show various examples of the use of the methods, including manifolds of the Lorenz ODE and other dynamical systems.