Local stable/unstable sets at a hyperbolic fixed point (set-level Hadamard–Perron)

stable_unstable_manifolds — a formalization challenge from the lean-eval benchmark.

Notes

For a C¹ map f : ℝⁿ → ℝⁿ with an invertible hyperbolic fixed point x₀ (no eigenvalue of dfₓ₀ on the unit circle, plus invertibility to exclude the degenerate zero-eigenvalue case), some open neighbourhood U ∋ x₀ carries the genuinely local stable set Wˢ = {x | ∀ k, f^[k] x ∈ U ∧ f^[k] x → x₀} and the local unstable set Wᵘ = {x | ∃ backward orbit y with y 0 = x, y k ∈ U for all k, and y → x₀}, with Wˢ ∩ Wᵘ = {x₀}. The 'orbit stays in U' clause is essential: without it, homoclinic points (forward and backward limit x₀ with excursions outside U) would falsify Wˢ ∩ Wᵘ = {x₀} in systems with homoclinic dynamics. This submission ships the set-level topological shadow of Hadamard–Perron; the full theorem additionally asserts that Wˢ, Wᵘ are immersed C¹ submanifolds tangent to the stable/unstable eigenspaces (same proof difficulty), which this Lean statement does not encode. §104 of Knill's Some Fundamental Theorems in Mathematics.

Formal statement

/-- **Local stable and unstable sets at a hyperbolic fixed point**
(set-level Hadamard–Perron). For a `C¹` map `f` with an invertible
hyperbolic fixed point at `x₀`, some open neighbourhood `U ∋ x₀`
carries the local stable set `Wˢ` (points whose forward orbit stays in
`U` and converges to `x₀`) and the local unstable set `Wᵘ` (points
admitting a backward orbit staying in `U` and converging to `x₀`), and
`Wˢ ∩ Wᵘ = {x₀}`. -/
theorem stable_unstable_manifolds_exist (n : ℕ) (f : E n → E n) (x₀ : E n)
    (_hf : ContDiffAt ℝ 1 f x₀)
    (_hfix : f x₀ = x₀)
    (_hhyp : IsHyperbolicLinear (fderiv ℝ f x₀))
    (_hf_inv : (fderiv ℝ f x₀).IsInvertible) :
    ∃ U : Set (E n), IsOpen U ∧ x₀ ∈ U ∧
      ∃ Ws Wu : Set (E n),
        Ws = {x | (∀ k : ℕ, f^[k] x ∈ U) ∧
                  Tendsto (fun k => f^[k] x) atTop (𝓝 x₀)} ∧
        Wu = {x | ∃ y : ℕ → E n,
                    y 0 = x ∧
                    (∀ k : ℕ, y k ∈ U) ∧
                    (∀ k : ℕ, f (y (k + 1)) = y k) ∧
                    Tendsto y atTop (𝓝 x₀)} ∧
        Ws ∩ Wu = {x₀} := by
  sorry

Informal solution sketch

The Hadamard graph-transform proof: write f near x₀ as f(x₀ + v) = x₀ + A v + g(v) with A = df(x₀), g(v) = o(‖v‖). The hyperbolic splitting ℝⁿ = Eˢ ⊕ Eᵘ (stable / unstable eigenspaces of A) lets one parametrise the candidate Wˢ as the graph of a Lipschitz function σ : Eˢ → Eᵘ near 0, with σ(0) = 0. The graph transform G(σ) := graph of (the new function whose graph is f(graph σ) ∩ small box) is a contraction on the Banach space of Lipschitz functions Eˢ → Eᵘ of small Lipschitz constant, because the stable direction contracts under A and the unstable direction expands (Banach fixed point). The unique fixed-point graph is the local stable manifold; the same argument with f⁻¹ gives Wᵘ. Hyperbolicity forces Wˢ ∩ Wᵘ = {x₀}: a point on both has its forward iterates bounded (lying on the bounded Wˢ) and its backward iterates bounded too, but the hyperbolic splitting forces such doubly-bounded orbits to be {x₀}. Mathlib has fderiv, ContDiff, Filter.Tendsto, Polynomial.roots, and LinearMap.charpoly, but no Hadamard–Perron theorem, no graph-transform machinery, no stable/unstable manifold framework, and no IsHyperbolicLinear predicate.

Source

J. Hadamard, 'Sur l'itération et les solutions asymptotiques des équations différentielles', Bull. Soc. Math. France 29 (1901); O. Perron, 'Über Stabilität und asymptotisches Verhalten der Integrale von Differentialgleichungssystemen', Math. Z. 29 (1929) 129–160. Listed as §104 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: stable_unstable_manifolds_exist
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.