+ +
+
+ +
+
| Home | +
| About | +
| Submission | +
| Updating Entries | +
| Using Entries | +
| Search | +
| Statistics | +
| Index | +
| Download | +
+
+
+
+
+
+
+
+
+
+
+
+
+
++
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 |
|
+ Proof outline + Proof document + |
+
| + Browse theories + |
| + Download this entry + | +
| Older releases: + None + |