Convergence of a negative gradient trajectory

A negative gradient trajectory γ of f, followed forward in time and never leaving a compact set K, converges to a critical point of f provided that f has only finitely many critical points in K:

∃ p ∈ K, ∇ f p = 0 ∧ Tendsto γ atTop (𝓝 p).

This is the statement that makes the moduli spaces of the Morse complex — the trajectories running from one critical point to another — well defined objects at all, and it is where Lane M of the analytic Heegaard Floer roadmap turns the dynamical facts of TauCeti/Analysis/Calculus/Morse/GradientFlow.lean into the beginnings of a chain complex.

Some hypothesis beyond compactness is needed to pin the limit down. For a merely smooth f a negative gradient trajectory can spiral forever towards a circle of critical points, its ω-limit set being the whole circle and the trajectory having no limit at all; for an analytic f this is ruled out by Łojasiewicz's gradient inequality, and here it is ruled out by the Morse condition. The theorem below therefore assumes that f has only finitely many critical points in K, which is exactly what a Morse function on a compact set provides, by TauCeti.HasNondegenerateCriticalPointsOn.finite_setOfPred_fderiv_eq_zero.

The argument

The three steps are the classical ones (Audin--Damian, Chapter 2).

The energy converges. Along the trajectory f is antitone (TauCeti.IsIntegralCurveOn.antitoneOn_comp_neg_gradient) and is bounded below on K, so f ∘ γ has a limit.

The gradient dies. The trajectory is Lipschitz, with the bound on ‖∇ f‖ over K as its constant, and ∇ f is uniformly continuous on K; so if ‖∇ f (γ t)‖ ≥ ε at some time t, the same holds with ε / 2 throughout a time interval [t, t + δ] whose length δ does not depend on t. The energy identity TauCeti.IsIntegralCurveOn.integral_norm_gradient_sq_eq_sub then makes f drop by at least δ (ε / 2) ^ 2 across that interval — impossible infinitely often, since the energy converges. Hence ∇ f (γ t) → 0.

The ω-limit set is a point. Every cluster point of γ along atTop is therefore a critical point in K, so the ω-limit set is finite; and it is preconnected, by TauCeti.isPreconnected_setOf_mapClusterPt_atTop. A finite preconnected set is a single point (Set.Finite.isTotallyDisconnected), and a map into a compact set with a unique cluster point converges to it.

Main results

• TauCeti.IsIntegralCurveOn.exists_tendsto_comp_atTop: the energy f ∘ γ converges.
• TauCeti.IsIntegralCurveOn.tendsto_gradient_atTop: the gradient along the trajectory tends to 0.
• TauCeti.IsIntegralCurveOn.gradient_eq_zero_of_mapClusterPt: every point of the ω-limit set is a critical point.
• TauCeti.IsIntegralCurveOn.exists_tendsto_atTop: a confined negative gradient trajectory converges to a critical point, when the critical points in the confining compact set are finite in number.
• TauCeti.IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn: the Morse form of the same statement, where the finiteness comes from nondegeneracy.
• TauCeti.IsIntegralCurveOn.exists_tendsto_atBot: the corresponding backward-time statement.
• TauCeti.IsIntegralCurveOn.exists_tendsto_atBot_of_hasNondegenerateCriticalPointsOn: its Morse form, where finiteness follows from nondegeneracy.

References

• M. Audin, M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• S. Łojasiewicz, Ensembles semi-analytiques, IHÉS, 1965, for the gradient inequality that replaces the finiteness hypothesis used here when f is analytic.
• Heegaard Floer homology roadmap, Lane M, "Morse homology".

The trajectory is Lipschitz

theorem TauCeti.IsIntegralCurveOn.norm_sub_le_of_norm_gradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} {C : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hC : ∀ y ∈ K, ‖gradient f y‖ ≤ C) {s t : ℝ} (hs : s ∈ Set.Ici 0) (ht : t ∈ Set.Ici 0) : ‖γ t - γ s‖ ≤ C * ‖t - s‖

A negative gradient trajectory confined to a compact set is Lipschitz, with any bound for the gradient on that set as its constant: the velocity is the negative gradient and therefore has the same norm as the gradient.

The energy converges

theorem TauCeti.IsIntegralCurveOn.exists_tendsto_comp_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) : ∃ (c : ℝ), Filter.Tendsto (fun (t : ℝ) => f (γ t)) Filter.atTop (nhds c)

The value of f along a confined negative gradient trajectory converges. It is antitone along the trajectory and bounded below on the compact set the trajectory never leaves.

The gradient dies along the trajectory

theorem TauCeti.IsIntegralCurveOn.tendsto_gradient_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) K) : Filter.Tendsto (fun (t : ℝ) => gradient f (γ t)) Filter.atTop (nhds 0)

The gradient tends to zero along a confined negative gradient trajectory.

The trajectory is Lipschitz and ∇ f is uniformly continuous on the compact set it stays in, so a time at which ‖∇ f (γ t)‖ is at least ε is the start of a time interval of a fixed length δ on which it is at least ε / 2. Across such an interval the energy identity makes f drop by at least δ (ε / 2) ^ 2; but the drops of f across intervals of fixed length tend to 0, because f converges along the trajectory. So the times at which ‖∇ f (γ t)‖ ≥ ε are bounded.

The ω-limit set

theorem TauCeti.IsIntegralCurveOn.gradient_eq_zero_of_mapClusterPt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} {x : E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) K) (hx : MapClusterPt x Filter.atTop γ) : gradient f x = 0

Every cluster point of a confined negative gradient trajectory is a critical point. The gradient tends to 0 along the trajectory, so the trajectory eventually lies in the closed set where ‖∇ f‖ ≤ ε, and hence so does every one of its cluster points.

Convergence

theorem TauCeti.IsIntegralCurveOn.exists_tendsto_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) K) (hfin : {y : E | y ∈ K ∧ gradient f y = 0}.Finite) : ∃ p ∈ K, gradient f p = 0 ∧ Filter.Tendsto γ Filter.atTop (nhds p)

A negative gradient trajectory that never leaves a compact set converges to a critical point of f in it, provided f has only finitely many critical points there.

Some such hypothesis is needed: a negative gradient trajectory can spiral forever towards a circle of critical points and then have no limit, its ω-limit set being the whole circle. The finiteness holds for a Morse function, which is TauCeti.IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn below.

Nothing is claimed about the rate of convergence, nor about the backward limit: the reversed curve fun t ↦ γ (-t) is a negative gradient trajectory of -f, so the backward limit is this same theorem applied to -f, whose hypotheses have to be checked separately.

theorem TauCeti.IsIntegralCurveOn.exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Ici 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hfderiv : ContinuousOn (fderiv ℝ f) K) (hM : HasNondegenerateCriticalPointsOn f K) : ∃ p ∈ K, gradient f p = 0 ∧ Filter.Tendsto γ Filter.atTop (nhds p)

The Morse form of the convergence theorem. A negative gradient trajectory confined to a compact set on which fderiv ℝ f is continuous and every critical point of f is nondegenerate converges to a critical point of f in that set.

Nondegeneracy enters only through the finiteness of the critical locus, which is TauCeti.HasNondegenerateCriticalPointsOn.finite_setOfPred_fderiv_eq_zero; the differentiability and the continuity of the gradient are read off the continuity of fderiv ℝ f on K, the gradient being the differential transported by the Riesz isometry.

theorem TauCeti.IsIntegralCurveOn.exists_tendsto_atBot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Iic 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hgrad : ContinuousOn (gradient f) K) (hfin : {y : E | y ∈ K ∧ gradient f y = 0}.Finite) : ∃ p ∈ K, gradient f p = 0 ∧ Filter.Tendsto γ Filter.atBot (nhds p)

A negative gradient trajectory confined to a compact set converges backwards to a critical point, provided the critical locus in that set is finite. Under these compactness, regularity, and finiteness hypotheses, this is the backward-time counterpart of exists_tendsto_atTop and gives a critical endpoint as t tends to -∞.

theorem TauCeti.IsIntegralCurveOn.exists_tendsto_atBot_of_hasNondegenerateCriticalPointsOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {K : Set E} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic 0)) (hK : IsCompact K) (hmaps : Set.MapsTo γ (Set.Iic 0) K) (hdiff : ∀ y ∈ K, DifferentiableAt ℝ f y) (hfderiv : ContinuousOn (fderiv ℝ f) K) (hM : HasNondegenerateCriticalPointsOn f K) : ∃ p ∈ K, gradient f p = 0 ∧ Filter.Tendsto γ Filter.atBot (nhds p)

The Morse form of backward convergence. A negative gradient trajectory confined to a compact set on which fderiv ℝ f is continuous and every critical point is nondegenerate converges backwards to a critical point in that set.

As in exists_tendsto_atTop_of_hasNondegenerateCriticalPointsOn, nondegeneracy is used only to obtain finiteness of the critical locus.