Peixoto: finitude of attractors for flows on orientable surfaces
OpenPalisConjecture.peixoto_orientable_surface_flowsattractorsdynamical-systems
Let be a compact, connected, Hausdorff, boundaryless, orientable smooth surface (), and let . There is a -dense set of vector fields on such that for every the flow of has finitely many attractors whose basins cover Lebesgue-almost all of .
This is the flow version of the Palis conjecture on orientable surfaces. It follows from Peixoto's theorem (1962): Morse–Smale vector fields are open and dense in . For a Morse–Smale field the attractors are the sinks and the attracting closed orbits. Every other point lies in the stable set of a saddle, a source or a repelling orbit, and the union of these stable sets is a finite union of points and curves.
Preamble
import Mathlib import Definitions.Def_palis_lebesgue_null import Definitions.Def_palis_attractor import Definitions.Def_palis_vector_field import Definitions.Def_palis_cr_topology import Definitions.Def_palis_orientable open scoped Manifold ContDiff
Formal statement
namespace PalisConjecture
theorem peixoto_orientable_surface_flows {M : Type*} [TopologicalSpace M] [T2Space M]
[CompactSpace M] [ConnectedSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M]
[IsManifold (𝓡 2) ∞ M] (hM : IsOrientable 2 M) (r : ℕ) (hr : 1 ≤ r) :
∃ D : Set ((x : M) → TangentSpace (𝓡 2) x), (∀ X ∈ D, IsCrVectorField r X) ∧
IsCrDenseVF r D ∧
∀ X ∈ D, ∀ Φ : ℝ → M → M, IsFlowOf X Φ → FlowHasFiniteAttractorsCoveringAE 2 Φ := by
sorry
end PalisConjecture
Source
Open Problem Garden, "Jacob Palis Conjecture (Finitude of Attractors) (Dynamical Systems)", posted by Jailton Viana, April 24, 2013, https://www.openproblemgarden.org/op/jacob_palis_conjecture_finitude_of_attractors_dynamical_systems (Conjecture box and the Definition of attractor below it); bibliography: C. Bonatti, L. J. Diaz, M. Viana, Dynamics Beyond Uniform Hyperbolicity, Encyclopaedia of Mathematical Sciences 102, Springer, 2005.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.