RIGOROUS VERIFICATION OF TRAJECTORIES FOR THE COMPUTER-SIMULATION OF DYNAMIC-SYSTEMS

We present a new technique for constructing a computer-assisted proof of the reliability of a long computer-generated trajectory of a dynamical system. Auxiliary calculations made along the noise-corrupted computer trajectory determine whether there exists a true trajectory which follows the computed trajectory closely for long times. A major application is to verify trajectories of chaotic differential equations and discrete systems. We apply the main results to computer simulations of the Henon map and the forced damped pendulum.