Exponential convergence of a negative gradient trajectory on a manifold

Let f be a function on a manifold M carrying a continuous Riemannian metric, and let p be a nondegenerate critical point of f. Near p the Morse form of Łojasiewicz's gradient inequality holds with the optimal exponent 1/2:

lam * |f y - f p| ≤ ‖grad f y‖ ^ 2

(TauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq). It is transported from the normed-space inequality TauCeti.IsNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_fderiv_sq for the coordinate expression of f in the preferred chart at p: near p the differential of that expression is bounded by a multiple of the Riemannian length of the gradient (TauCeti.Manifold.eventually_norm_fderiv_comp_extChartAt_symm_le_mul_norm_mgradient). The metric need not be adapted to the chart, nor smooth.

Now let γ be the maximal integral curve of -grad f through x, defined for all positive time and converging to p. The energy f (γ t) - f p is nonnegative (TauCeti.le_comp_maximalIntegralCurve_neg_mgradient), since f decreases along γ and tends to f p. Its derivative is -‖grad f (γ t)‖ ^ 2, which the inequality above bounds by -lam times the energy once γ stays near p, so by Grönwall's inequality the energy decays like exp (-lam * t) (TauCeti.exists_sub_le_mul_exp_maximalIntegralCurve_neg_mgradient). This is the manifold counterpart, for an arbitrary C¹ metric, of the vector-space theorem IsIntegralCurveOn.exists_sub_le_mul_exp_atTop.

Energy decay alone does not bound the distance from γ t to p, since the Hessian at a saddle has null directions. The distance is recovered from the Riemannian length of γ. The length over [a, b] is at most sqrt (2 * (b - a) * E), where E is the path energy ½ ∫ ‖γ'‖² of γ on [a, b] (ContMDiffOn.pathELength_le_ofReal_sqrt_energy), and along a negative gradient trajectory 2 * E = f (γ a) - f (γ b) (TauCeti.energy_maximalIntegralCurve_neg_mgradient). Over each unit of time the square root of f (γ t) - f p shrinks by the factor exp (-lam / 2), so summing a geometric series bounds the tail length of γ after time t, and with it the Riemannian distance from γ t to p, by a multiple of sqrt (f (γ t) - f p). Hence that distance decays exponentially (TauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient), as in IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atTop. The distance is Manifold.riemannianEDist, the infimum of lengths of C¹ paths; on a Riemannian manifold in the sense of IsRiemannianManifold it is the ambient extended distance.

Combined with the convergence theorems of TauCeti.Geometry.Manifold.Morse.GradientFlow, this gives exponential convergence without assuming convergence. A forward trajectory trapped in a compact set K whose critical points are all nondegenerate converges exponentially fast to a critical point in K (TauCeti.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient): such a K contains only finitely many critical points, so the trajectory has a limit, which is nondegenerate. In particular every forward negative gradient trajectory of a proper Morse function bounded below converges exponentially fast to a critical point (IsMorse.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient).

Main results

• TauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq: the Łojasiewicz inequality with exponent 1/2 near a nondegenerate critical point, for the Riemannian gradient.
• TauCeti.le_comp_maximalIntegralCurve_neg_mgradient: the energy along a forward negative gradient trajectory is bounded below by its value at the limit point.
• TauCeti.exists_sub_le_mul_exp_maximalIntegralCurve_neg_mgradient: along a forward negative gradient trajectory converging to a nondegenerate critical point the energy decays exponentially.
• TauCeti.exists_pathELength_le_mul_sqrt_maximalIntegralCurve_neg_mgradient and TauCeti.exists_riemannianEDist_le_mul_sqrt_maximalIntegralCurve_neg_mgradient: the tail length of a trajectory converging to a nondegenerate critical point, and its Riemannian distance to the limit, are bounded by a multiple of the square root of the energy.
• TauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient: such a trajectory converges to its limit exponentially fast in the Riemannian distance.
• TauCeti.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient: a forward trajectory trapped in a compact set with only nondegenerate critical points converges exponentially fast to one of them.
• IsMorse.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient: every forward negative gradient trajectory of a proper Morse function bounded below converges exponentially fast to a critical point.

References

• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, Les Équations aux Dérivées Partielles, Éditions du CNRS, Paris, 1963, 87--89.
• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

theorem TauCeti.IsManifoldNondegenerateCriticalPoint.exists_mul_abs_sub_le_norm_mgradient_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {f : M → ℝ} {p : M} (hp : IsManifoldNondegenerateCriticalPoint I f p) : ∃ lam > 0, ∀ᶠ (y : M) in nhds p, lam * |f y - f p| ≤ ‖Manifold.mgradient I f y‖ ^ 2

The Morse form of Łojasiewicz's gradient inequality on a Riemannian manifold. Near a nondegenerate critical point p of f, the absolute energy difference |f y - f p| is bounded by a multiple of the squared Riemannian length of the gradient of f at y, for any continuous Riemannian metric.

theorem TauCeti.le_comp_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x p : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) (hconv : Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)) {t : ℝ} (ht : 0 ≤ t) : f p ≤ f (maximalIntegralCurve (-Manifold.mgradient I f) x t)

The energy along a convergent trajectory is nonnegative. If the maximal integral curve of -grad f through x exists for all positive time and converges to p, then f p ≤ f (γ t) for every t ≥ 0: the function f decreases along the curve and tends to f p.

theorem TauCeti.exists_sub_le_mul_exp_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x p : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hp : IsManifoldNondegenerateCriticalPoint I f p) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) (hconv : Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, f (maximalIntegralCurve (-Manifold.mgradient I f) x t) - f p ≤ C * Real.exp (-(μ * t))

The energy along a trajectory converging to a nondegenerate critical point decays exponentially. If the maximal integral curve γ of -grad f through x exists for all positive time and converges to a nondegenerate critical point p, then f (γ t) - f p ≤ C * exp (-μ * t) for some μ, C > 0 and all large t.

Length of a trajectory and distance to its limit

theorem TauCeti.exists_pathELength_le_mul_sqrt_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x p : M} (hp : IsManifoldNondegenerateCriticalPoint I f p) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) (hconv : Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : ∃ K > 0, ∀ᶠ (t : ℝ) in Filter.atTop, ∀ (s : ℝ), Manifold.pathELength I (maximalIntegralCurve (-Manifold.mgradient I f) x) t s ≤ ENNReal.ofReal (K * √(f (maximalIntegralCurve (-Manifold.mgradient I f) x t) - f p))

The tail length of a trajectory converging to a nondegenerate critical point is controlled by the square root of its energy. If the maximal integral curve γ of -grad f through x exists for all positive time and converges to a nondegenerate critical point p, then for some K > 0 and all large t, every piece of γ starting at time t has Riemannian length at most K * sqrt (f (γ t) - f p).

theorem TauCeti.exists_riemannianEDist_le_mul_sqrt_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x p : M} (hp : IsManifoldNondegenerateCriticalPoint I f p) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) (hconv : Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : ∃ K > 0, ∀ᶠ (t : ℝ) in Filter.atTop, Manifold.riemannianEDist I (maximalIntegralCurve (-Manifold.mgradient I f) x t) p ≤ ENNReal.ofReal (K * √(f (maximalIntegralCurve (-Manifold.mgradient I f) x t) - f p))

The Riemannian distance from a trajectory to its nondegenerate limit is controlled by the square root of its energy. If the maximal integral curve γ of -grad f through x exists for all positive time and converges to a nondegenerate critical point p, then for some K > 0 and all large t, the Riemannian distance from γ t to p is at most K * sqrt (f (γ t) - f p).

theorem TauCeti.exists_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [BoundarylessManifold I M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x p : M} (hp : IsManifoldNondegenerateCriticalPoint I f p) (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) (hconv : Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, Manifold.riemannianEDist I (maximalIntegralCurve (-Manifold.mgradient I f) x t) p ≤ ENNReal.ofReal (C * Real.exp (-(μ * t)))

A trajectory converging to a nondegenerate critical point converges exponentially fast in the Riemannian distance. If the maximal integral curve γ of -grad f through x exists for all positive time and converges to a nondegenerate critical point p, then the Riemannian distance from γ t to p is at most C * exp (-μ * t) for some μ, C > 0 and all large t. This is the manifold counterpart, for an arbitrary C¹ metric, of the vector-space theorem IsIntegralCurveOn.exists_norm_sub_le_mul_exp_atTop.

Trapped trajectories and proper Morse functions

theorem TauCeti.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} {K : Set M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x ∩ Set.Ici 0) K) (hnd : ∀ y ∈ criticalPoints I f ∩ K, IsManifoldNondegenerateCriticalPoint I f y) : ∃ p ∈ criticalPoints I f ∩ K, Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p) ∧ ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, Manifold.riemannianEDist I (maximalIntegralCurve (-Manifold.mgradient I f) x t) p ≤ ENNReal.ofReal (C * Real.exp (-(μ * t)))

A trapped trajectory converges exponentially fast. If the forward part of the maximal integral curve γ of -grad f through x stays in a compact set K all of whose critical points are nondegenerate, then γ converges to a critical point p in K, and the Riemannian distance from γ t to p is at most C * exp (-μ * t) for some μ, C > 0 and all large t. The metric is an arbitrary C¹ metric, M need not be compact, and the limit may be a saddle.

theorem TauCeti.IsMorse.exists_tendsto_and_riemannianEDist_le_mul_exp_maximalIntegralCurve_neg_mgradient {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} (hf : IsMorse I f) (hp : IsProperMap f) (hbdd : BddBelow (Set.range f)) (x : M) : ∃ p ∈ criticalPoints I f, Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p) ∧ ∃ μ > 0, ∃ C > 0, ∀ᶠ (t : ℝ) in Filter.atTop, Manifold.riemannianEDist I (maximalIntegralCurve (-Manifold.mgradient I f) x t) p ≤ ENNReal.ofReal (C * Real.exp (-(μ * t)))

Negative gradient trajectories of a proper Morse function converge exponentially fast. If f is a proper Morse function bounded below, the maximal integral curve of -grad f through any point x converges to a critical point p of f, and the Riemannian distance from its value at time t to p is at most C * exp (-μ * t) for some μ, C > 0 and all large t, for any C¹ Riemannian metric.