SciCADE 2011 - Minisymposia

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.

SPEAKERS
Markus Neher, Karlsruhe Institute of Technology, Germany	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.