Convergence of negative gradient trajectories trapped in a compact set

Let f be a C² function on a boundaryless finite-dimensional manifold M carrying a C¹ Riemannian metric, and let γ be the maximal integral curve of the negative gradient -grad f through a point x. Neither M nor the sublevels of f need be compact, and the metric need not be complete. Along γ the function f decreases with derivative -‖grad f‖² (TauCeti.hasDerivAt_comp_maximalIntegralCurve_neg_mgradient); this is the energy dissipation identity, whose integrated form identifies the total energy ∫ ‖grad f (γ t)‖² dt with the drop of f (TauCeti.integral_Ioi_norm_mgradient_sq_maximalIntegralCurve).

Suppose that the forward trajectory of x stays in a compact set K. Then it exists for all positive time, every cluster point of γ t as t → ∞ is a critical point of f, and if K contains only finitely many critical points the trajectory converges to one of them (TauCeti.exists_tendsto_maximalIntegralCurve_neg_mgradient). This is the manifold counterpart, for an arbitrary Riemannian metric, of the vector-space theorem IsIntegralCurveOn.exists_tendsto_atTop. The ω-limit set of the trajectory is nonempty, connected and invariant under the local flow, and f is constant on it, so the gradient vanishes there.

A proper Morse function bounded below traps each forward trajectory in its initial compact sublevel, so every forward negative gradient trajectory of such a function converges to a critical point (TauCeti.IsMorse.exists_tendsto_maximalIntegralCurve_neg_mgradient). The metric is arbitrary: it need not be adapted to the Morse charts of f.

Main declarations

• TauCeti.contMDiffOn_maximalIntegralCurve_neg_mgradient: a negative gradient trajectory is C¹ on its interval of definition.
• TauCeti.hasDerivAt_comp_maximalIntegralCurve_neg_mgradient and TauCeti.antitoneOn_comp_maximalIntegralCurve_neg_mgradient: energy dissipation and monotonicity along a negative gradient trajectory.
• TauCeti.energy_maximalIntegralCurve_neg_mgradient: over a bounded time interval the energy ½ ∫ ‖γ'‖² of a negative gradient trajectory is half the drop of f.
• TauCeti.integrableOn_Ioi_norm_mgradient_sq_maximalIntegralCurve and TauCeti.integral_Ioi_norm_mgradient_sq_maximalIntegralCurve: the energy of a forward trajectory along which f has a limit is finite, and equals the drop of f.
• TauCeti.mapsTo_maximalIntegralCurve_neg_mgradient_preimage_Iic: a forward trajectory stays in the sublevel of its initial point.
• TauCeti.Ici_subset_maximalIntegralCurveInterval_neg_mgradient: a trapped forward trajectory exists for all positive time.
• TauCeti.mem_criticalPoints_of_mapClusterPt_maximalIntegralCurve_neg_mgradient: the ω-limit points of a trapped forward trajectory are critical.
• TauCeti.exists_tendsto_maximalIntegralCurve_neg_mgradient: a trapped forward trajectory converges to a critical point when only finitely many critical points lie in the trap.
• TauCeti.IsMorse.exists_tendsto_maximalIntegralCurve_neg_mgradient: every forward negative gradient trajectory of a proper Morse function bounded below converges to a critical point.

References

• M. W. Hirsch, S. Smale and R. L. Devaney, Differential Equations, Dynamical Systems, and an Introduction to Chaos, second edition, Academic Press, 2004, Chapter 9 (gradient systems).
• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Proposition 2.1.6.

theorem TauCeti.contMDiffOn_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 : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x)

The maximal integral curve of -grad f is C¹ on its interval of definition.

Energy dissipation

theorem TauCeti.hasDerivAt_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 : M} {t : ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (ht : t ∈ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) : HasDerivAt (fun (s : ℝ) => f (maximalIntegralCurve (-Manifold.mgradient I f) x s)) (-‖Manifold.mgradient I f (maximalIntegralCurve (-Manifold.mgradient I f) x t)‖ ^ 2) t

Energy dissipation along a negative gradient trajectory. Along the maximal integral curve γ of -grad f, the function f has derivative -‖grad f (γ t)‖².

theorem TauCeti.antitoneOn_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 : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : AntitoneOn (fun (s : ℝ) => f (maximalIntegralCurve (-Manifold.mgradient I f) x s)) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x)

Energy monotonicity. The function f is antitone along the maximal integral curve of its negative gradient.

theorem TauCeti.mapsTo_maximalIntegralCurve_neg_mgradient_preimage_Iic {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 : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : Set.MapsTo (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x ∩ Set.Ici 0) (f ⁻¹' Set.Iic (f x))

A forward trajectory stays in the sublevel of its initial point. The forward part of the maximal integral curve of -grad f through x lies in the sublevel {y | f y ≤ f x}.

theorem TauCeti.energy_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 : M} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) {a b : ℝ} (hab : Set.uIcc a b ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) : Manifold.energy I (maximalIntegralCurve (-Manifold.mgradient I f) x) a b = (f (maximalIntegralCurve (-Manifold.mgradient I f) x a) - f (maximalIntegralCurve (-Manifold.mgradient I f) x b)) / 2

The energy identity on a bounded time interval. Between two times a and b of its interval of definition, the energy ½ ∫ ‖γ'‖² of the maximal integral curve γ of -grad f is half the drop f (γ a) - f (γ b).

theorem TauCeti.integrableOn_Ioi_norm_mgradient_sq_maximalIntegralCurve {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 : M} (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) {c : ℝ} (hc : Filter.Tendsto (fun (s : ℝ) => f (maximalIntegralCurve (-Manifold.mgradient I f) x s)) Filter.atTop (nhds c)) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : MeasureTheory.IntegrableOn (fun (s : ℝ) => ‖Manifold.mgradient I f (maximalIntegralCurve (-Manifold.mgradient I f) x s)‖ ^ 2) (Set.Ioi 0) MeasureTheory.volume

The energy of a forward trajectory is finite. If the maximal integral curve of -grad f through x exists for all positive time and f has a limit along it, then ‖grad f‖² is integrable along it on (0, ∞).

theorem TauCeti.integral_Ioi_norm_mgradient_sq_maximalIntegralCurve {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 : M} (hx : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x) {c : ℝ} (hc : Filter.Tendsto (fun (s : ℝ) => f (maximalIntegralCurve (-Manifold.mgradient I f) x s)) Filter.atTop (nhds c)) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : ∫ (s : ℝ) in Set.Ioi 0, ‖Manifold.mgradient I f (maximalIntegralCurve (-Manifold.mgradient I f) x s)‖ ^ 2 = f x - c

The energy identity. If the maximal integral curve of -grad f through x exists for all positive time and f tends to c along it, then ∫₀^∞ ‖grad f (γ t)‖² dt = f x - c.

Trapped trajectories

theorem TauCeti.Ici_subset_maximalIntegralCurveInterval_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 : M} {K : Set M} (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x ∩ Set.Ici 0) K) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) : Set.Ici 0 ⊆ maximalIntegralCurveInterval (-Manifold.mgradient I f) x

A trapped forward trajectory exists for all positive time. If the forward part of the maximal integral curve of -grad f through x stays in a compact set, it is defined on [0, ∞).

theorem TauCeti.mem_criticalPoints_of_mapClusterPt_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 : M} {K : Set M} (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x ∩ Set.Ici 0) K) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) {z : M} (hz : MapClusterPt z Filter.atTop (maximalIntegralCurve (-Manifold.mgradient I f) x)) : z ∈ criticalPoints I f

The ω-limit points of a trapped trajectory are critical. If the forward part of the maximal integral curve of -grad f through x stays in a compact set, every cluster point of this curve as t → ∞ is a critical point of f.

theorem TauCeti.exists_tendsto_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 : M} {K : Set M} (hK : IsCompact K) (hmem : Set.MapsTo (maximalIntegralCurve (-Manifold.mgradient I f) x) (maximalIntegralCurveInterval (-Manifold.mgradient I f) x ∩ Set.Ici 0) K) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hfin : (criticalPoints I f ∩ K).Finite) : ∃ p ∈ criticalPoints I f ∩ K, Filter.Tendsto (maximalIntegralCurve (-Manifold.mgradient I f) x) Filter.atTop (nhds p)

Convergence of a trapped negative gradient trajectory. If the forward part of the maximal integral curve of -grad f through x stays in a compact set K containing only finitely many critical points of f, the trajectory converges to one of these critical points. That it exists for all positive time is TauCeti.Ici_subset_maximalIntegralCurveInterval_neg_mgradient.

theorem TauCeti.IsMorse.exists_tendsto_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 → ℝ} (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)

Negative gradient trajectories of a proper Morse function converge. If f is a proper Morse function bounded below, the maximal integral curve of -grad f through any point converges to a critical point of f, for any C¹ Riemannian metric.