Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: The Poincaré-Bendixson Theorem


view this post on Zulip Email Gateway (Aug 22 2022 at 21:09):

From: Tobias Nipkow <nipkow@in.tum.de>
The Poincaré-Bendixson Theorem
Fabian Immler and Yong Kiam Tan

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.

https://www.isa-afp.org/entries/Poincare_Bendixson.html

Enjoy!
smime.p7s


Last updated: Apr 23 2024 at 12:29 UTC