Rigorous Computational Dynamics
mini chomp
The existence of chaotic dynamics was first demonstrated by Poincare more than a century ago. Its relevance to science and engineering exploded 50 years ago with the advent of the computer and the ability to simulate concrete nonlinear systems. This in turn stimulated the development of the very rich and beautiful theory of dynamical systems. And yet, given a particular nonlinear ODE any comprehensive understanding of the associated dynamics is typically obtained through numerical methods which are not rigorous and may be misleading in some critical cases of particular interest. Motivated by this quandary we are working on developing the analytic and computational foundations for computer assisted proofs in ODEs.
topological measurements of the structure of invariant sets
 
Coarse, topological measurements of dynamical systems defined by maps can be used to uncover information about invariant sets for the system.  These techniques are based on the Conley index and have been used to detect invariant structures from fixed points and periodic orbits, to connecting orbits and sets which exhibit chaotic symbolic dynamics.  More notably, these techniques have been used to study both finite-dimensional and infinite-dimensional systems and to prove the existence of unstable invariant sets. The method relies on first building a pair of compact sets called anindex pair and then computing the relative homology of the pair.  This information is then used to make conclusions about the associated invariant structures.  
One of the most efficient methods for determining the equilibria of a continuous parameterized family of differential equations is to use predictor-corrector continuation techniques. In the case of partial differential equations this procedure must be applied to some finite dimensional approximation which of course raises the question of the validity of the output. We introduce a new technique that combines the information obtained from the predictor-corrector steps with ideas from rigorous computations and verifies that the numerically produced equilibrium for the finite dimensional system can be used to explicitly define a set which contains a unique equilibrium for the infinite dimensional partial differential equation.
A method based on the Conley index theory for proving the existence of periodic trajectories in a smooth dynamical system in Euclidean space is developed. This method can be applied in the cases where a hyperbolic periodic orbit is numerically observed. The method uses cubical index pairs and requires the computation of the map induced in homology by the cubical index map.