Continuous normalization of connecting gradient trajectories

An intermediate value of a Morse function selects one time on every connecting orbit. The selected time varies continuously with the initial point, so shifting each point to that time gives a continuous map into the level slice. This supplies the topological part of the unparametrized trajectory-space construction; smooth manifold charts require further work.

The level-slice viewpoint follows Audin--Damian, Morse Theory and Floer Homology, Chapter 2.

theorem Flow.IsNegativeGradient.exists_continuous_levelCrossingTime {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ x ∈ φ.unstableSet p ∩ φ.stableSet q, DifferentiableAt ℝ f x) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) {c : ℝ} (hc : f q < c ∧ c < f p) : ∃ (t : ↑(φ.unstableSet p ∩ φ.stableSet q) → ℝ), Continuous t ∧ ∀ (x : ↑(φ.unstableSet p ∩ φ.stableSet q)), f (φ.toFun (t x) ↑x) = c

The unique time at which a connecting trajectory meets an intermediate level depends continuously on its initial point.

theorem Flow.IsNegativeGradient.exists_continuous_levelSlice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {φ : Flow ℝ E} {f : E → ℝ} {p q : E} (hφ : φ.IsNegativeGradient f) (hf : ∀ x ∈ φ.unstableSet p ∩ φ.stableSet q, DifferentiableAt ℝ f x) (hfp : ContinuousAt f p) (hfq : ContinuousAt f q) {c : ℝ} (hc : f q < c ∧ c < f p) : ∃ (s : ↑(φ.unstableSet p ∩ φ.stableSet q) → ↑(φ.unstableSet p ∩ φ.stableSet q ∩ {x : E | f x = c})), Continuous s ∧ (∀ (x : ↑(φ.unstableSet p ∩ φ.stableSet q)), ↑(s x) ∈ φ.orbit ↑x) ∧ (∀ (x : ↑(φ.unstableSet p ∩ φ.stableSet q)), f ↑x = c → ↑(s x) = ↑x) ∧ ∀ (x : ↑(φ.unstableSet p ∩ φ.stableSet q)) (u : ℝ), s ⟨φ.toFun u ↑x, ⋯⟩ = s x

Moving each connecting point to its unique intersection with an intermediate level is continuous, fixes points already on that level, and is invariant under time translation.