Applicability of the Interval Taylor Model to the Computational Proof of Existence of Periodic Trajectories in Systems of Ordinary Differential Equations

We consider the construction of the interval Taylor model used to prove the existence of periodic trajectories in systems of ordinary differential equations. Our model differs from the ones available in the literature in the method for describing the algorithms for the computation of arithmetic operations over Taylor models. In the framework of the current model, this permits reducing the computational expenditures for obtaining interval estimates on computers. We prove an assertion that permits establishing the existence of a periodic solution of a system of ordinary differential equations by verifying the convergence of the Picard iterations in the sense of embedding of the proposed Taylor models. An example illustrating how the resulting assertion can be used to prove the existence of a closed trajectory in the van der Pol system is given.