The Poincaré-Bendixson Theorem

 

Title: The Poincaré-Bendixson Theorem
Authors: Fabian Immler and Yong Kiam Tan
Submission date: 2019-12-18
Abstract: The Poincaré-Bendixson theorem is a classical result in the study of (continuous) dynamical systems. Colloquially, it restricts the possible behaviors of planar dynamical systems: such systems cannot be chaotic. In practice, it is a useful tool for proving the existence of (limiting) periodic behavior in planar systems. The theorem is an interesting and challenging benchmark for formalized mathematics because proofs in the literature rely on geometric sketches and only hint at symmetric cases. It also requires a substantial background of mathematical theories, e.g., the Jordan curve theorem, real analysis, ordinary differential equations, and limiting (long-term) behavior of dynamical systems.
BibTeX:
@article{Poincare_Bendixson-AFP,
  author  = {Fabian Immler and Yong Kiam Tan},
  title   = {The Poincaré-Bendixson Theorem},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/Poincare_Bendixson.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Ordinary_Differential_Equations