Treffer: Phase Portraits of Planar Vector Fields: Computer Proofs

This paper presents a general approach to the problem of producing computer-generated proofs for the correctness of phase portraits for structurally stable vector fields. This approach was initiated by Salvador Malo [1993], and we develop it further. The algorithms we describe have been implemented and tested with a few examples. They have been effective in producing the desired proofs, perhaps far more so than other methods that have been attempted with these types of problems. The difficulty with producing rigorous bounds on the location of trajectories lies in the growth of error estimates during highly iterative procedures. Numerical integration algorithms of a typical trajectory may involve thousands of time steps in such an iterative procedure. Controlling roundoff errors of floating-point computations in such a process is problematic. Successful efforts to prove statements about the approximate location of trajectories have tended to rely upon very high numerical precision of the numerical integration as an antidote to the rapid growth of error estimates. Such precise numerical analysis has been based on the use of interval arithmetic. The basic operations of interval arithmetic produce intervals that contain the range of a function on rectangular domains. Our methods for proving properties of planar vector fields also make use of interval arithmetic, but they do so in a much more limited way. In particular, we refrain from iterative calculations with interval arithmetic. Geometric structures are computed that we expect to possess qualitative properties (like transversality) with respect to the original vector field. Validation of these properties utilizes interval arithmetic, but the computational complexity of each unit of interval arithmetic computation is ind.