
MINISYMPOSIA 
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.
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 Taylormodel based methods and the rigorous verified integrator
COSYVI 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 1E6. The resulting flows can be used for the study
of dynamics using discretizations and graphbased 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 HighOrder 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 highorder 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.

