From local invariant disks to global stable sets

Near a nondegenerate critical point, the Lyapunov--Perron construction identifies the initial conditions of confined forward and backward trajectories with disks tangent to the positive and negative Hessian subspaces. This file relates those local disks to the global stable and unstable sets of a negative-gradient flow.

When the gradient is globally Lipschitz, uniqueness identifies every confined local trajectory with an orbit of the global flow. Conversely, a trajectory converging to the critical point eventually enters, and thereafter remains in, each sufficiently small ball. Consequently the global stable or unstable set is exactly the union of the complete flow orbits through its local disk. This is the local-to-global step used when the stable and unstable sets are given their manifold structures and intersected to form Morse trajectory spaces.

Main declarations

• mem_localInvariantSet_iff_negativeGradientFlow: characterizes a local invariant set over an order-connected time set using the global flow.
• stableSet_eq_biUnion_orbit_localInvariantSet_Ici: a convergent forward local invariant set generates the global stable set under the flow.
• unstableSet_eq_biUnion_orbit_localInvariantSet_Iic: the backward-time counterpart.
• IsNondegenerateCriticalPoint.stableSet_eq_biUnion_orbit_localStableSet and IsNondegenerateCriticalPoint.unstableSet_eq_biUnion_orbit_localUnstableSet: the corresponding statements for the local Lyapunov--Perron sets.
• IsNondegenerateCriticalPoint.exists_stableSet_eq_biUnion_orbit_localStableSet and IsNondegenerateCriticalPoint.exists_unstableSet_eq_biUnion_orbit_localUnstableSet: positive radii for which the local sets generate the global stable and unstable sets.
• IsNondegenerateCriticalPoint.isEmbedding_stableGraph_orbit and IsNondegenerateCriticalPoint.isEmbedding_unstableGraph_orbit: flowing a graph over the stable or unstable spectral subspace gives another topological embedding.
• contDiffAt_negativeGradientFlow_graph: when a graph and the function are C¹ and C² respectively, its transported parameterization is C¹.

References

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

theorem TauCeti.mem_localInvariantSet_iff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {s : Set ℝ} (hs : s.OrdConnected) (h0 : 0 ∈ s) {r rho : ℝ} {z : E} : z ∈ localInvariantSet f x s Q r rho ↔ (∀ t ∈ s, (negativeGradientFlow f hf).toFun t (x + z) - x ∈ Metric.closedBall 0 r) ∧ ‖Q z‖ ≤ rho

Membership in a local invariant set over an order-connected time set containing zero can be witnessed by the global negative-gradient orbit: the orbit stays in the chosen ball throughout the time set and its initial projection obeys the cutoff.

theorem TauCeti.mem_localInvariantSet_Ici_iff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} {z : E} : z ∈ localInvariantSet f x (Set.Ici 0) Q r rho ↔ (∀ (t : ℝ), 0 ≤ t → (negativeGradientFlow f hf).toFun t (x + z) - x ∈ Metric.closedBall 0 r) ∧ ‖Q z‖ ≤ rho

Membership in a forward local invariant set can be witnessed by the global negative-gradient orbit, with the confinement condition imposed at nonnegative times.

theorem TauCeti.mem_localInvariantSet_Iic_iff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} {z : E} : z ∈ localInvariantSet f x (Set.Iic 0) Q r rho ↔ (∀ t ≤ 0, (negativeGradientFlow f hf).toFun t (x + z) - x ∈ Metric.closedBall 0 r) ∧ ‖Q z‖ ≤ rho

Membership in a backward local invariant set can be witnessed by the global negative-gradient orbit, with the confinement condition imposed at nonpositive times.

theorem TauCeti.image_add_localInvariantSet_Ici_subset_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Ici 0) → Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atTop (nhds 0)) : (fun (z : E) => x + z) '' localInvariantSet f x (Set.Ici 0) Q r rho ⊆ (negativeGradientFlow f hf).stableSet x

Translating a forward local invariant set back to the base point gives points in the global stable set, provided every trajectory confined to the chosen ball converges.

theorem TauCeti.image_add_localInvariantSet_Iic_subset_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Iic 0) → Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atBot (nhds 0)) : (fun (z : E) => x + z) '' localInvariantSet f x (Set.Iic 0) Q r rho ⊆ (negativeGradientFlow f hf).unstableSet x

Translating a backward local invariant set back to the base point gives points in the global unstable set, provided every trajectory confined to the chosen ball converges backward.

theorem TauCeti.exists_negativeGradientFlow_sub_mem_localInvariantSet_Ici_of_mem_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) {p : E} (hp : p ∈ (negativeGradientFlow f hf).stableSet x) : ∃ (T : ℝ), (negativeGradientFlow f hf).toFun T p - x ∈ localInvariantSet f x (Set.Ici 0) Q r rho

Every point in the global stable set has a time translate whose displacement belongs to a given forward local invariant set with positive cutoffs.

theorem TauCeti.exists_negativeGradientFlow_sub_mem_localInvariantSet_Iic_of_mem_unstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) {p : E} (hp : p ∈ (negativeGradientFlow f hf).unstableSet x) : ∃ (T : ℝ), (negativeGradientFlow f hf).toFun T p - x ∈ localInvariantSet f x (Set.Iic 0) Q r rho

Every point in the global unstable set has a time translate whose displacement belongs to a given backward local invariant set with positive cutoffs.

theorem TauCeti.stableSet_eq_biUnion_orbit_localInvariantSet_Ici {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Ici 0) → Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atTop (nhds 0)) : (negativeGradientFlow f hf).stableSet x = ⋃ z ∈ localInvariantSet f x (Set.Ici 0) Q r rho, (negativeGradientFlow f hf).orbit (x + z)

A forward local invariant set whose confined trajectories converge generates the whole global stable set under the negative-gradient flow.

theorem TauCeti.unstableSet_eq_biUnion_orbit_localInvariantSet_Iic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (Q : E →L[ℝ] E) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Iic 0) → Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atBot (nhds 0)) : (negativeGradientFlow f hf).unstableSet x = ⋃ z ∈ localInvariantSet f x (Set.Iic 0) Q r rho, (negativeGradientFlow f hf).orbit (x + z)

A backward local invariant set whose confined trajectories converge generates the whole global unstable set under the negative-gradient flow.

theorem TauCeti.contDiffAt_negativeGradientFlow_graph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} (hf : LipschitzWith K (gradient f)) (hfs : ContDiff ℝ 2 f) {g : E → E} {v : E} (hg : ContDiffAt ℝ 1 g v) (t : ℝ) : ContDiffAt ℝ 1 (fun (w : E) => (negativeGradientFlow f hf).toFun t (x + (w + g w))) v

A C¹ graph remains C¹ after transport by any fixed time of a globally defined negative-gradient flow of a C² function. This applies to both the stable and unstable graph maps at a Morse critical point.

theorem TauCeti.IsNondegenerateCriticalPoint.isEmbedding_stableGraph_orbit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) (g : E → E) (hPg : ∀ v ∈ (↑h.stableProjection).range, h.stableProjection (g v) = 0) (hg : ContinuousOn g ↑(↑h.stableProjection).range) (t : ℝ) : Topology.IsEmbedding fun (v : ↥(↑h.stableProjection).range) => (negativeGradientFlow f hf).toFun t (x + (↑v + g ↑v))

Flowing an embedded graph over the stable spectral subspace gives another embedding, providing the topological half of transporting a local stable disk along an orbit.

theorem TauCeti.IsNondegenerateCriticalPoint.isEmbedding_unstableGraph_orbit {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) (g : E → E) (hPg : ∀ v ∈ (↑h.unstableProjection).range, h.unstableProjection (g v) = 0) (hg : ContinuousOn g ↑(↑h.unstableProjection).range) (t : ℝ) : Topology.IsEmbedding fun (v : ↥(↑h.unstableProjection).range) => (negativeGradientFlow f hf).toFun t (x + (↑v + g ↑v))

Flowing an embedded graph over the unstable spectral subspace gives another embedding.

theorem TauCeti.IsNondegenerateCriticalPoint.mem_localStableSet_iff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) {r rho : ℝ} {z : E} : z ∈ h.localStableSet r rho ↔ (∀ (t : ℝ), 0 ≤ t → (negativeGradientFlow f hf).toFun t (x + z) - x ∈ Metric.closedBall 0 r) ∧ ‖h.stableProjection z‖ ≤ rho

Membership in the local stable set is equivalent to confinement of the global negative-gradient orbit together with the stable-projection cutoff.

theorem TauCeti.IsNondegenerateCriticalPoint.mem_localUnstableSet_iff_negativeGradientFlow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) {r rho : ℝ} {z : E} : z ∈ h.localUnstableSet r rho ↔ (∀ t ≤ 0, (negativeGradientFlow f hf).toFun t (x + z) - x ∈ Metric.closedBall 0 r) ∧ ‖h.unstableProjection z‖ ≤ rho

Membership in the local unstable set is equivalent to confinement of the global negative-gradient orbit together with the unstable-projection cutoff.

theorem TauCeti.IsNondegenerateCriticalPoint.stableSet_eq_biUnion_orbit_localStableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Ici 0) → Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atTop (nhds 0)) : (negativeGradientFlow f hf).stableSet x = ⋃ z ∈ h.localStableSet r rho, (negativeGradientFlow f hf).orbit (x + z)

A local stable set whose confined trajectories converge generates the whole global stable set under the negative-gradient flow.

theorem TauCeti.IsNondegenerateCriticalPoint.unstableSet_eq_biUnion_orbit_localUnstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) {r rho : ℝ} (hr : 0 < r) (hrho : 0 < rho) (hconv : ∀ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Iic 0) → Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r) → Filter.Tendsto y Filter.atBot (nhds 0)) : (negativeGradientFlow f hf).unstableSet x = ⋃ z ∈ h.localUnstableSet r rho, (negativeGradientFlow f hf).orbit (x + z)

A local unstable set whose confined trajectories converge backward generates the whole global unstable set under the negative-gradient flow.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_stableSet_eq_biUnion_orbit_localStableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) : ∃ r > 0, ∃ rho > 0, (negativeGradientFlow f hf).stableSet x = ⋃ z ∈ h.localStableSet r rho, (negativeGradientFlow f hf).orbit (x + z)

There are positive radii for which the local stable set generates the whole global stable set under the negative-gradient flow.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_unstableSet_eq_biUnion_orbit_localUnstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {K : NNReal} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hf : LipschitzWith K (gradient f)) : ∃ r > 0, ∃ rho > 0, (negativeGradientFlow f hf).unstableSet x = ⋃ z ∈ h.localUnstableSet r rho, (negativeGradientFlow f hf).orbit (x + z)

There are positive radii for which the local unstable set generates the whole global unstable set under the negative-gradient flow.