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

stable_unstable_manifolds

Submitter: Kim Morrison.

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*.

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).

Informal solution: 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.

theorem declaration uses `sorry`stable_unstable_manifolds_exist (n : ℕ) (f : LeanEval.Dynamics.StableUnstableManifoldsProblem.E n → LeanEval.Dynamics.StableUnstableManifoldsProblem.E n) (x₀ : LeanEval.Dynamics.StableUnstableManifoldsProblem.E n)
    (_hf : ContDiffAt ℝ 1 f x₀)
    (_hfix : f x₀ = x₀)
    (_hhyp : LeanEval.Dynamics.StableUnstableManifoldsProblem.IsHyperbolicLinear (fderiv ℝ f x₀))
    (_hf_inv : (fderiv ℝ f x₀).IsInvertible) :
    ∃ U : Set (LeanEval.Dynamics.StableUnstableManifoldsProblem.E n), IsOpen U ∧ x₀ ∈ U ∧
      ∃ Ws Wu : Set (LeanEval.Dynamics.StableUnstableManifoldsProblem.E n),
        Ws = {x | (∀ k : ℕ, f^[k] x ∈ U) ∧
                  Tendsto (fun k => f^[k] x) atTop (𝓝 x₀)} ∧
        Wu = {x | ∃ y : ℕ → LeanEval.Dynamics.StableUnstableManifoldsProblem.E n,
                    y 0 = x ∧
                    (∀ k : ℕ, y k ∈ U) ∧
                    (∀ k : ℕ, f (y (k + 1)) = y k) ∧
                    Tendsto y atTop (𝓝 x₀)} ∧
        Ws ∩ Wu = {x₀} := byn:ℕf:E n → E nx₀:E n_hf:ContDiffAt ℝ 1 f x₀_hfix:f x₀ = x₀_hhyp:IsHyperbolicLinear (fderiv ℝ f x₀)_hf_inv:(fderiv ℝ f x₀).IsInvertible⊢ ∃ U,
  IsOpen U ∧
    x₀ ∈ U ∧
      ∃ Ws Wu,
        Ws = {x | (∀ (k : ℕ), f^[k] x ∈ U) ∧ Tendsto (fun k => f^[k] x) atTop (𝓝 x₀)} ∧
          Wu = {x | ∃ y, y 0 = x ∧ (∀ (k : ℕ), y k ∈ U) ∧ (∀ (k : ℕ), f (y (k + 1)) = y k) ∧ Tendsto y atTop (𝓝 x₀)} ∧
            Ws ∩ Wu = {x₀}
  sorryAll goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 5, 2026

• @GanjinZero with Seed Prover (ByteDance) on Jun 5, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 5, 2026