Prove2Me

Anosov diffeomorphisms are CrC^r structurally stable

Open
StabilityConjecture.anosov_structurally_stable

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-topologydynamical-systems

Let MM be a closed manifold: a compact Hausdorff smooth manifold without boundary, modelled on Rn\mathbb R^n. Let r≥1r\ge 1 and let f∈Diffr(M)f\in\mathrm{Diff}^r(M) be an Anosov diffeomorphism: MM itself is a hyperbolic set of ff. Then ff is CrC^r structurally stable: there is a neighbourhood U\mathcal U of ff in Diffr(M)\mathrm{Diff}^r(M) such that every g∈Ug\in\mathcal U is topologically conjugate to ff,

∃ h ⁣:M→M homeomorphism with h∘f=g∘h.\exists\, h\colon M\to M \text{ homeomorphism with } h\circ f=g\circ h .

This is the first and simplest case of the converse direction of the Palis–Smale conjecture: hyperbolicity implies structural stability.

Preamble
import Mathlib
import Definitions.Def_ClosingLemma_DiffeoCrTopology
import Definitions.Def_PughClosingLemma_nonwandering
import Definitions.Def_StabilityConjecture_Basic

open scoped Manifold ContDiff Topology
Formal statement
namespace StabilityConjecture

open ClosingLemma

theorem anosov_structurally_stable {n : ℕ} {M : Type*} [TopologicalSpace M] [T2Space M]
    [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M]
    (r : ℕ) (hr : 1 ≤ r) (f : Diff n M r) (hf : IsAnosov f) :
    IsStructurallyStable r f := by sorry

end StabilityConjecture
Source
D. V. Anosov, Geodesic flows on closed Riemannian manifolds with negative curvature, Proc. Steklov Inst. Math. 90 (1967). Context: Open Problem Garden, "C^r Stability Conjecture" (Conjecture, author(s) J. Palis and S. Smale; posted by m n, December 20th, 2007), https://www.openproblemgarden.org/op/c_r_stability_conjecture
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