Computer Assisted Proof of Drift Orbits Along Normally Hyperbolic Manifolds

Normally hyperbolic invariant manifolds theory provides an efficient tool for proving diffusion in dynamical systems. In this paper we develop a methodology for computer assisted proofs of diffusion in a-priori chaotic systems based on this approach. We devise a method, which allows us to validate the needed conditions in a finite number of steps, which can be performed by a computer by means of rigorous-interval-arithmetic computations. We apply our method to the generalized standard map, obtaining diffusion over an explicit range of actions.