
The
PoincaréBendixson
Theorem
Title: 
The PoincaréBendixson Theorem 
Authors:

Fabian Immler and
Yong Kiam Tan

Submission date: 
20191218 
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 (longterm) behavior of
dynamical systems. 
BibTeX: 
@article{Poincare_BendixsonAFP,
author = {Fabian Immler and Yong Kiam Tan},
title = {The PoincaréBendixson Theorem},
journal = {Archive of Formal Proofs},
month = dec,
year = 2019,
note = {\url{http://isaafp.org/entries/Poincare_Bendixson.html},
Formal proof development},
ISSN = {2150914x},
}

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.

