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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.