Global stable and unstable sets are embedded C¹ submanifolds

Let x be a nondegenerate critical point of a globally C² function f on a finite-dimensional real inner product space whose gradient is globally Lipschitz. This file shows that the stable and unstable sets of x under the negative-gradient flow are embedded C¹ submanifolds of the ambient space: every point of the stable set has a C¹ ambient chart, with C¹ inverse, carrying the stable set onto the stable Hessian subspace, and likewise for the unstable set. Their dimensions are finrank E - morseIndex f x and morseIndex f x (IsNondegenerateCriticalPoint.finrank_stableLinearSubspace_add_morseIndex and finrank_unstableLinearSubspace).

The proof has two steps.

• Near x the stable set is the local stable disk. Since a nondegenerate critical point is isolated, ‖∇ f‖ is bounded below by some c > 0 on a thin annulus around x. A trajectory that crosses the annulus loses at least c times its width in value (Flow.IsNegativeGradient.dist_le_of_mem_stableSet), so a point of the stable set close to x and with value close to f x never leaves the ball: it belongs to the confined local stable set of the Lyapunov--Perron construction.
• Transport along the flow. A point y of the stable set reaches, at some time T, the neighbourhood of x where the previous step applies and where the local straightening chart of IsNondegenerateCriticalPoint.exists_localStableSet_chart is defined. Composing that chart with the time-T flow, a C¹ diffeomorphism of the ambient space, straightens the stable set around y.

Without the first step the transported chart would only straighten the part of the stable set lying in the transported local disk; points of the stable set accumulating from far along the flow could otherwise break embeddedness. For a gradient flow they cannot.

Main declarations

• IsNondegenerateCriticalPoint.eventually_forall_dist_le_of_mem_stableSet and IsNondegenerateCriticalPoint.eventually_forall_dist_le_of_mem_unstableSet: near a nondegenerate critical point, stable and unstable trajectories stay in a given ball.
• IsNondegenerateCriticalPoint.exists_stableSet_chart: every point of the global stable set has a C¹ straightening chart onto the stable Hessian subspace.
• IsNondegenerateCriticalPoint.exists_unstableSet_chart: the same for the unstable set and the unstable Hessian subspace.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_forall_dist_le_of_mem_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {φ : Flow ℝ E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) (hd : Differentiable ℝ f) {r : ℝ} (hr : 0 < r) : ∀ᶠ (z : E) in nhds x, z ∈ φ.stableSet x → ∀ (t : ℝ), 0 ≤ t → dist (φ.toFun t z) x ≤ r

Near a nondegenerate critical point, stable trajectories stay close. For every radius r > 0, every point near the critical point x whose negative-gradient trajectory converges to x remains within distance r of x at all nonnegative times. Thus, near x, the stable set coincides with the local stable set of trajectories confined to a ball.

theorem TauCeti.IsNondegenerateCriticalPoint.eventually_forall_dist_le_of_mem_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} {φ : Flow ℝ E} (h : IsNondegenerateCriticalPoint f x) (hφ : φ.IsNegativeGradient f) (hd : Differentiable ℝ f) {r : ℝ} (hr : 0 < r) : ∀ᶠ (z : E) in nhds x, z ∈ φ.unstableSet x → ∀ t ≤ 0, dist (φ.toFun t z) x ≤ r

Near a nondegenerate critical point, unstable trajectories stay close in backward time. The backward-time counterpart of IsNondegenerateCriticalPoint.eventually_forall_dist_le_of_mem_stableSet.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_stableSet_chart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} [CompleteSpace E] {K : NNReal} (h : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) {y : E} (hy : y ∈ (negativeGradientFlow f hf).stableSet x) : ∃ (e : OpenPartialHomeomorph E E), y ∈ e.source ∧ (∀ z ∈ e.source, ContDiffAt ℝ 1 (↑e) z) ∧ (∀ z ∈ e.target, ContDiffAt ℝ 1 (↑e.symm) z) ∧ ∀ z ∈ e.source, z ∈ (negativeGradientFlow f hf).stableSet x ↔ ↑e z ∈ ⋯.stableLinearSubspace

The stable set of a Morse critical point is an embedded C¹ submanifold. For a globally C² function with globally Lipschitz gradient, every point y of the stable set of a nondegenerate critical point x under the negative-gradient flow has a C¹ ambient chart, with C¹ inverse, carrying the stable set onto the stable Hessian subspace, whose dimension is finrank E - morseIndex f x.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_unstableSet_chart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} [CompleteSpace E] {K : NNReal} (h : IsNondegenerateCriticalPoint f x) (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) {y : E} (hy : y ∈ (negativeGradientFlow f hf).unstableSet x) : ∃ (e : OpenPartialHomeomorph E E), y ∈ e.source ∧ (∀ z ∈ e.source, ContDiffAt ℝ 1 (↑e) z) ∧ (∀ z ∈ e.target, ContDiffAt ℝ 1 (↑e.symm) z) ∧ ∀ z ∈ e.source, z ∈ (negativeGradientFlow f hf).unstableSet x ↔ ↑e z ∈ ⋯.unstableLinearSubspace

The unstable set of a Morse critical point is an embedded C¹ submanifold. The backward-time counterpart of IsNondegenerateCriticalPoint.exists_stableSet_chart: every point of the unstable set has a C¹ ambient chart, with C¹ inverse, carrying the unstable set onto the unstable Hessian subspace, whose dimension is the Morse index.