Local invariant sets at a Morse critical point

At a nondegenerate critical point x of a twice continuously differentiable function on a finite-dimensional real Hilbert space, the negative-gradient vector field in displacement coordinates splits as

-hessianOperator f x z + negativeGradientRemainder f x (x + z).

The Hessian spectral splitting supplies a continuous projection onto the stable linear subspace and exponential estimates for the linear term. The nonlinear remainder has arbitrarily small Lipschitz constant on a sufficiently small ball. This file combines those facts with the local Lyapunov--Perron theorem: the initial displacements of forward negative-gradient trajectories confined to that ball form a Lipschitz graph over a ball in the stable linear subspace.

This is a local stable-manifold theorem at the equilibrium: the graph map is Lipschitz, differentiable at the origin with derivative zero, and hence tangent there to the stable linear subspace. It is moreover continuously differentiable at every point of the closed ball over which the set is a graph, since on a small enough ball the remainder is C¹ with uniformly continuous derivative (ContinuousLinearMap.contDiffAt_localStableGraphMap). The embedded-submanifold structure carried by this C¹ graph, and its globalization along the flow, are not established here.

Applying the same construction after reversing time gives the corresponding local unstable set as the graph of a Lipschitz, C¹ map tangent at the origin to the unstable Hessian spectral subspace.

Because the projection inverts the graph parameterization, each of the two sets is homeomorphic to a closed ball in the spectral subspace it is a graph over, hence to a Euclidean closed ball of the dimension of that subspace. This is where the Morse index acquires its geometric meaning: the local unstable set is a disk of dimension the Morse index, and the local stable set a disk of complementary dimension. At the two extreme indices one of the disks is a single point: the zero displacement, which is the critical point x in these centred coordinates and, as soon as both radii are nonnegative, belongs to both sets.

Main declarations

• localInvariantSet: the displacements from which a solution of the centred negative-gradient equation stays in a given ball throughout a given time set, truncated by a norm bound on a projection, together with its forward and backward instances at a nondegenerate critical point, IsNondegenerateCriticalPoint.localStableSet and IsNondegenerateCriticalPoint.localUnstableSet.
• IsNondegenerateCriticalPoint.exists_localStableSet_eq_lipschitzGraph: confined forward trajectories in coordinates centred at a nondegenerate critical point form the graph of a Lipschitz map that is C¹ over the whole graph domain, tangent at the origin to the stable Hessian spectral subspace.
• IsNondegenerateCriticalPoint.exists_localUnstableSet_eq_lipschitzGraph: the backward-time counterpart, tangent at the origin to the unstable Hessian spectral subspace.
• IsNondegenerateCriticalPoint.exists_localStableSet_homeomorph_closedBall and IsNondegenerateCriticalPoint.exists_localUnstableSet_homeomorph_closedBall: the two sets are closed disks of dimension the ambient dimension minus the Morse index, respectively the Morse index.
• zero_mem_localInvariantSet, with IsNondegenerateCriticalPoint.zero_mem_localStableSet and IsNondegenerateCriticalPoint.zero_mem_localUnstableSet: every such set with nonnegative radii contains the zero displacement, which is the critical point x in centred coordinates.
• IsNondegenerateCriticalPoint.exists_localUnstableSet_eq_singleton_of_morseIndex_eq_zero and IsNondegenerateCriticalPoint.exists_localStableSet_eq_singleton_of_morseIndex_eq_finrank: at a local minimum, respectively a local maximum, the degenerate one of the two disks is exactly the zero displacement.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• C. Chicone, Ordinary Differential Equations with Applications, 2nd ed., Springer, 2006, Section 4.3.

def TauCeti.localInvariantSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : E → ℝ) (x : E) (s : Set ℝ) (Q : E →L[ℝ] E) (r rho : ℝ) : Set E

The displacements z from which the centred negative-gradient equation z' = (-∇ f) (x + z) has a solution staying in closedBall 0 r for all times in s, truncated by the bound ‖Q z‖ ≤ rho. The local stable and unstable sets at a nondegenerate critical point are the two instances of this set that the Lyapunov--Perron construction describes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mem_localInvariantSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [CompleteSpace E] {s : Set ℝ} {Q : E →L[ℝ] E} {r rho : ℝ} {z : E} : z ∈ localInvariantSet f x s Q r rho ↔ (∃ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) s ∧ y 0 = z ∧ Set.MapsTo y s (Metric.closedBall 0 r)) ∧ ‖Q z‖ ≤ rho

theorem TauCeti.zero_mem_localInvariantSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [CompleteSpace E] (hx : gradient f x = 0) (s : Set ℝ) (Q : E →L[ℝ] E) {r rho : ℝ} (hr : 0 ≤ r) (hrho : 0 ≤ rho) : 0 ∈ localInvariantSet f x s Q r rho

At a critical point the zero displacement belongs to every such set with nonnegative radii, whatever the time set and the projection: the constant displacement trajectory y = 0, which represents the equilibrium at x, solves the centred equation and stays in every ball of nonnegative radius.

def TauCeti.IsNondegenerateCriticalPoint.localStableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (r rho : ℝ) : Set E

The local stable set at a nondegenerate critical point: the displacements from which the centred negative-gradient equation has a forward solution staying in closedBall 0 r, truncated by the bound ‖stableProjection z‖ ≤ rho.

Equations

• h.localStableSet r rho = TauCeti.localInvariantSet f x (Set.Ici 0) h.stableProjection r rho

def TauCeti.IsNondegenerateCriticalPoint.localUnstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (r rho : ℝ) : Set E

The local unstable set at a nondegenerate critical point: the displacements from which the centred negative-gradient equation has a backward solution staying in closedBall 0 r, truncated by the bound ‖unstableProjection z‖ ≤ rho.

Equations

• h.localUnstableSet r rho = TauCeti.localInvariantSet f x (Set.Iic 0) h.unstableProjection r rho

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.mem_localStableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] {h : IsNondegenerateCriticalPoint f x} {r rho : ℝ} {z : E} : z ∈ h.localStableSet r rho ↔ (∃ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Ici 0) ∧ y 0 = z ∧ Set.MapsTo y (Set.Ici 0) (Metric.closedBall 0 r)) ∧ ‖h.stableProjection z‖ ≤ rho

@[simp]

theorem TauCeti.IsNondegenerateCriticalPoint.mem_localUnstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] {h : IsNondegenerateCriticalPoint f x} {r rho : ℝ} {z : E} : z ∈ h.localUnstableSet r rho ↔ (∃ (y : ℝ → E), IsIntegralCurveOn y (fun (x_1 : ℝ) (w : E) => (-gradient f) (x + w)) (Set.Iic 0) ∧ y 0 = z ∧ Set.MapsTo y (Set.Iic 0) (Metric.closedBall 0 r)) ∧ ‖h.unstableProjection z‖ ≤ rho

theorem TauCeti.IsNondegenerateCriticalPoint.localStableSet_eq_localInvariantSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (r rho : ℝ) : h.localStableSet r rho = localInvariantSet f x (Set.Ici 0) h.stableProjection r rho

The local stable set is the forward local invariant set cut out by the stable projection.

theorem TauCeti.IsNondegenerateCriticalPoint.localUnstableSet_eq_localInvariantSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (r rho : ℝ) : h.localUnstableSet r rho = localInvariantSet f x (Set.Iic 0) h.unstableProjection r rho

The local unstable set is the backward local invariant set cut out by the unstable projection.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localStableSet_eq_lipschitzGraph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (C : NNReal) (hC : 0 < C) : ∃ r > 0, ∃ rho > 0, ∃ (g : E → E), LipschitzWith C g ∧ g 0 = 0 ∧ HasFDerivAt g 0 0 ∧ (∀ v ∈ Metric.closedBall 0 rho, ContDiffAt ℝ 1 g v) ∧ (∀ (v : E), h.stableProjection (g v) = 0) ∧ (∀ (v : E), g (h.stableProjection v) = g v) ∧ h.localStableSet r rho = (fun (v : E) => v + g v) '' (↑⋯.stableLinearSubspace ∩ Metric.closedBall 0 rho) ∧ ∀ (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)

Confined trajectories at a Morse critical point form a C¹ Lipschitz graph. For every positive Lipschitz constant C, there are positive radii r and rho such that the initial displacements of forward solutions of the centred negative-gradient equation that remain in closedBall 0 r, restricted by norm (stableProjection z) ≤ rho, are exactly the graph of a C-Lipschitz map over stableLinearSubspace ∩ closedBall 0 rho.

The graph map is continuously differentiable at every point of closedBall 0 rho. It vanishes at the origin, has derivative zero there, takes values in the unstable linear subspace (the kernel of the stable projection), and depends only on the stable component of its input. Thus its graph is tangent at the origin to the stable linear subspace. The same radius r also guarantees that every confined solution tends to zero.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localUnstableSet_eq_lipschitzGraph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (C : NNReal) (hC : 0 < C) : ∃ r > 0, ∃ rho > 0, ∃ (g : E → E), LipschitzWith C g ∧ g 0 = 0 ∧ HasFDerivAt g 0 0 ∧ (∀ v ∈ Metric.closedBall 0 rho, ContDiffAt ℝ 1 g v) ∧ (∀ (v : E), h.unstableProjection (g v) = 0) ∧ (∀ (v : E), g (h.unstableProjection v) = g v) ∧ h.localUnstableSet r rho = (fun (v : E) => v + g v) '' (↑⋯.unstableLinearSubspace ∩ Metric.closedBall 0 rho) ∧ ∀ (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)

Confined backward trajectories at a Morse critical point form a C¹ Lipschitz graph. For every positive Lipschitz constant C, there are positive radii r and rho such that the initial displacements of backward solutions of the centred negative-gradient equation that stay in closedBall 0 r, restricted by norm (unstableProjection z) ≤ rho, are exactly the graph of a C-Lipschitz map over unstableLinearSubspace ∩ closedBall 0 rho.

The graph map is continuously differentiable at every point of closedBall 0 rho. It vanishes at the origin, has derivative zero there, takes values in the stable linear subspace (the kernel of the unstable projection), and depends only on the unstable component of its input. Thus its graph is tangent at the origin to the unstable linear subspace. Every such confined backward solution tends to zero in backward time.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localStableSet_homeomorph_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : ∃ r > 0, ∃ rho > 0, Nonempty (↑(h.localStableSet r rho) ≃ₜ ↑(Metric.closedBall 0 rho))

The local stable set at a Morse critical point is a closed disk whose dimension is the ambient dimension less the Morse index. For suitable radii r and rho, the initial displacements of forward negative-gradient solutions confined to closedBall 0 r and restricted by norm (stableProjection z) ≤ rho are homeomorphic to a closed ball of that dimension.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localUnstableSet_homeomorph_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) : ∃ r > 0, ∃ rho > 0, Nonempty (↑(h.localUnstableSet r rho) ≃ₜ ↑(Metric.closedBall 0 rho))

The local unstable set at a Morse critical point is a closed disk whose dimension is the Morse index. For suitable radii r and rho, the initial displacements of backward negative-gradient solutions confined to closedBall 0 r and restricted by norm (unstableProjection z) ≤ rho are homeomorphic to a closed ball of that dimension.

theorem TauCeti.IsNondegenerateCriticalPoint.zero_mem_localStableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) {r rho : ℝ} (hr : 0 ≤ r) (hrho : 0 ≤ rho) : 0 ∈ h.localStableSet r rho

The zero displacement, which represents the critical point x in centred coordinates, lies in the local stable set of any nonnegative radii: the constant displacement trajectory y = 0 solves the centred negative-gradient equation and stays in every ball of nonnegative radius.

theorem TauCeti.IsNondegenerateCriticalPoint.zero_mem_localUnstableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) {r rho : ℝ} (hr : 0 ≤ r) (hrho : 0 ≤ rho) : 0 ∈ h.localUnstableSet r rho

The zero displacement, which represents the critical point x in centred coordinates, lies in the local unstable set of any nonnegative radii.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localUnstableSet_eq_singleton_of_morseIndex_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hind : morseIndex f x = 0) : ∃ r > 0, ∃ rho > 0, h.localUnstableSet r rho = {0}

At a local minimum the local unstable set degenerates to a point. A nondegenerate critical point of Morse index 0 has no unstable directions, so for suitable radii the zero displacement is the only admissible initial displacement of a backward negative-gradient solution confined near x.

theorem TauCeti.IsNondegenerateCriticalPoint.exists_localStableSet_eq_singleton_of_morseIndex_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} [FiniteDimensional ℝ E] (h : IsNondegenerateCriticalPoint f x) (hind : morseIndex f x = Module.finrank ℝ E) : ∃ r > 0, ∃ rho > 0, h.localStableSet r rho = {0}

At a local maximum the local stable set degenerates to a point. A nondegenerate critical point whose Morse index is the dimension of the ambient space has no stable directions, so for suitable radii the zero displacement is the only admissible initial displacement of a forward negative-gradient solution confined near x.