Convergence of the orbits of a flow with a Lyapunov function

Let φ be a flow of ℝ on a compact Hausdorff space and g a continuous function that is antitone along every orbit. Suppose that the points along whose orbit g is constant are contained in a finite set C. Then every orbit converges, forward in time, to a point of C.

This is the topological core of the convergence of gradient-like flows: for the flow of a pseudo-gradient field adapted to a Morse function f, the function is f and C is the finite set of critical points.

Main declarations

• Flow.exists_tendsto_atTop_of_antitone: every orbit converges forward in time to a point of C.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Proposition 2.1.6.

theorem Flow.exists_tendsto_atTop_of_antitone {α : Type u_1} [TopologicalSpace α] [CompactSpace α] [T2Space α] (φ : Flow ℝ α) {g : α → ℝ} (hg : Continuous g) (hanti : ∀ (y : α), Antitone fun (t : ℝ) => g (φ.toFun t y)) {C : Set α} (hC : C.Finite) (hrest : ∀ (z : α), (∀ (t : ℝ), g (φ.toFun t z) = g z) → z ∈ C) (y : α) : ∃ x ∈ C, Filter.Tendsto (fun (t : ℝ) => φ.toFun t y) Filter.atTop (nhds x)

The orbits of a flow with a Lyapunov function converge. Let g be a continuous function, antitone along every orbit of a flow φ of ℝ on a compact Hausdorff space. If the points along whose orbit g is constant are contained in a finite set C, every orbit converges forward in time to a point of C.