Regular levels along connecting gradient trajectories

For a flow in which critical points of the potential are rest points, a trajectory joining distinct limiting points never meets a critical point. Hence every point on such a trajectory is a regular point of the defining function. In particular, the intermediate level used to slice the time-translation action is regular at every connecting point on that level.

The rest-point hypothesis follows from uniqueness of trajectories, for example when the gradient is Lipschitz. Without uniqueness, a differentiable orbit of a non-Lipschitz vector field may pass through a rest point and continue. This regularity is the differential input for giving the level slice the smooth structure used in Morse trajectory spaces.

The trajectory-space construction follows M. Audin and M. Damian, Morse Theory and Floer Homology, Chapter 2.

theorem Flow.gradient_ne_zero_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hrest : ∀ (y : E), gradient f y = 0 → ∀ (t : ℝ), φ.toFun t y = y) (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : gradient f x ≠ 0

A connecting orbit between distinct endpoints contains no critical point when the gradient vanishes only at rest points. If it met one, the entire orbit would be constant.

theorem Flow.differentiableAt_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hrest : ∀ (y : E), gradient f y = 0 → ∀ (t : ℝ), φ.toFun t y = y) (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : DifferentiableAt ℝ f x

Every point of a connecting orbit between distinct endpoints is a differentiability point of the potential when critical points are rest points.

theorem Flow.fderiv_surjective_of_mem_unstableSet_inter_stableSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q x : E} (hrest : ∀ (y : E), gradient f y = 0 → ∀ (t : ℝ), φ.toFun t y = y) (hpq : p ≠ q) (hx : x ∈ φ.unstableSet p ∩ φ.stableSet q) : Function.Surjective ⇑(fderiv ℝ f x)

The derivative of the potential is surjective at every point on a connecting orbit between distinct endpoints. Thus each intermediate level is regular along the connecting set.