Exponential convergence of a negative gradient trajectory

A negative gradient trajectory that converges to a nondegenerate critical point p converges to it at an exponential rate:

‖γ t - p‖ ≤ C * exp (-μ * t) for large t,

and the same holds for the energy f (γ t) - f p. This is the asymptotic input the moduli spaces of Morse and Floer theory are built on: it is what puts a trajectory running between two critical points into the weighted Sobolev spaces on which the linearized operator d/ds + A(s) is Fredholm, and it is what makes the ends of a trajectory converge fast enough for the broken-trajectory compactness and gluing arguments that assemble the Morse and Floer complexes.

The argument

Everything rests on the Morse form of Łojasiewicz's gradient inequality, with the optimal exponent 1/2: near a nondegenerate critical point,

lam * |f x - f p| ≤ ‖∇ f x‖ ^ 2.

Both halves of it come from the linearization TauCeti.hessianOperator of the gradient. Since the Hessian operator is invertible, the gradient is bounded below by a multiple of the distance to p (TauCeti.IsNondegenerateCriticalPoint.exists_mul_norm_sub_le_norm_gradient); since it vanishes at p and is bounded above by a multiple of that distance, the mean value inequality bounds the energy by the square of the distance (ContDiffAt.exists_abs_sub_le_mul_norm_sub_sq, which needs no nondegeneracy). Comparing the two gives the inequality (TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq).

Along the trajectory the energy g t = f (γ t) - f p is nonnegative — f ∘ γ is antitone and tends to f p — and satisfies g' = -‖∇ f (γ t)‖ ^ 2 ≤ -lam * g, so g decays like exp (-lam * t).

That decay does not by itself bound ‖γ t - p‖: an indefinite quadratic approximation has null directions, so the energy difference does not uniformly control the squared distance to p. The distance is instead recovered from the length of the trajectory. On a time interval of length one the energy identity TauCeti.IsIntegralCurveOn.integral_norm_gradient_sq_eq_sub computes ∫ ‖∇ f (γ s)‖ ^ 2, and the elementary bound v ≤ (α * v ^ 2 + 1 / α) / 2, optimized in α, converts it into a bound for ∫ ‖∇ f (γ s)‖ = ∫ ‖γ' s‖, hence for ‖γ (t + 1) - γ t‖, by the square root of the energy. Summing the resulting geometric series over the times t, t + 1, t + 2, … and passing to the limit bounds ‖γ t - p‖ by a multiple of sqrt (g t), which decays like exp (-lam * t / 2).

Main results

• TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_gradient_sq: the Morse form of Łojasiewicz's gradient inequality, with exponent 1/2.
• TauCeti.IsIntegralCurveOn.exists_sub_le_mul_exp_atTop: the energy along a trajectory converging to a nondegenerate critical point decays exponentially.
• TauCeti.IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atTop: the trajectory itself converges exponentially fast.
• TauCeti.IsIntegralCurveOn.exists_norm_gradient_le_mul_exp_atTop and TauCeti.IsIntegralCurveOn.exists_norm_deriv_le_mul_exp_atTop: the gradient and velocity decay exponentially.
• The corresponding atBot theorems give backward-time energy, position, gradient, and velocity decay by reversing time and negating the function.

References

• M. Audin, M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.
• M. Schwarz, Morse Homology, Birkhäuser, 1993, Chapter 2, where the exponential convergence of trajectories is what places them in the weighted Sobolev spaces of the Fredholm theory.

Decay along a trajectory

The main theorems

theorem TauCeti.IsIntegralCurveOn.exists_sub_le_mul_exp_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atTop (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, f (γ t) - f p ≤ C * Real.exp (-(μ * t))

The energy along a trajectory converging to a nondegenerate critical point decays exponentially.

theorem TauCeti.IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atTop (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, ‖γ t - p‖ ≤ C * Real.exp (-(μ * t))

A negative gradient trajectory converging to a nondegenerate critical point converges to it exponentially fast. The rate is half the Łojasiewicz constant of the critical point, which for a nondegenerate critical point is controlled by the Hessian.

theorem TauCeti.IsIntegralCurveOn.exists_norm_gradient_le_mul_exp_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atTop (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, ‖gradient f (γ t)‖ ≤ C * Real.exp (-(μ * t))

The gradient along a trajectory converging to a nondegenerate critical point decays exponentially.

theorem TauCeti.IsIntegralCurveOn.exists_norm_deriv_le_mul_exp_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Ici a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atTop (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, ‖deriv γ t‖ ≤ C * Real.exp (-(μ * t))

The velocity of a trajectory converging to a nondegenerate critical point decays exponentially.

theorem TauCeti.IsIntegralCurveOn.exists_sub_le_mul_exp_atBot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atBot (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atBot, f p - f (γ t) ≤ C * Real.exp (μ * t)

The energy along a backward trajectory converging to a nondegenerate critical point decays exponentially.

theorem TauCeti.IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atBot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atBot (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atBot, ‖γ t - p‖ ≤ C * Real.exp (μ * t)

The backward-time form. A negative gradient trajectory converging to a nondegenerate critical point as t → -∞ converges to it exponentially fast. Reversing time turns the trajectory into a negative gradient trajectory of -f, whose critical point at p is again nondegenerate.

theorem TauCeti.IsIntegralCurveOn.exists_norm_gradient_le_mul_exp_atBot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atBot (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atBot, ‖gradient f (γ t)‖ ≤ C * Real.exp (μ * t)

The gradient along a backward trajectory converging to a nondegenerate critical point decays exponentially.

theorem TauCeti.IsIntegralCurveOn.exists_norm_deriv_le_mul_exp_atBot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {γ : ℝ → E} {p : E} {a : ℝ} (hγ : IsIntegralCurveOn γ (fun (x : ℝ) (x_1 : E) => -gradient f x_1) (Set.Iic a)) (hp : IsNondegenerateCriticalPoint f p) (hconv : Filter.Tendsto γ Filter.atBot (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atBot, ‖deriv γ t‖ ≤ C * Real.exp (μ * t)

The velocity of a backward trajectory converging to a nondegenerate critical point decays exponentially.