A hyperbolic sink is an attractor

Proved

PalisConjecture.sink_is_attractor

by Lucas · Oct 11, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

attractorsdynamical-systems

Let $M$ be a Hausdorff smooth manifold modelled on $\mathbb R^n$ , let $r\ge1$ , and let $f$ be a $C^r$ diffeomorphism of $M$ with a fixed point $p$ . Let $e$ be a chart of the atlas whose domain contains $p$ , and let $A=D(e\circ f\circ e^{-1})(e(p))$ be the derivative of $f$ at $p$ in this chart. If

\|A^N\|<1\quad\text{for some } N\ge0

(equivalently, every eigenvalue of $A$ has modulus $<1$ ), then $\{p\}$ is an attractor of $f$ .

This is the basic example of an attractor and shows that the attractor definition is satisfied by hyperbolic sinks, whose basins contain an open neighbourhood of $p$ .

Formalization Note The operator norm is taken with respect to the Euclidean norm on $\mathbb R^n$ .

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

open scoped Manifold ContDiff

Formal statement

namespace PalisConjecture

theorem sink_is_attractor (n : ℕ) {M : Type*} [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (r : ℕ) (hr : 1 ≤ r) (f : M ≃ₘ^(r : WithTop ℕ∞)⟮𝓡 n, 𝓡 n⟯ M) (p : M) (hp : f p = p)
    (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)))
    (he : e ∈ atlas (EuclideanSpace ℝ (Fin n)) M) (hpe : p ∈ e.source)
    (hsink : ∃ N : ℕ, ‖(fderiv ℝ (e ∘ f ∘ e.symm) (e p)) ^ N‖ < 1) :
    IsAttractor n (f : M → M) {p} := 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

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph