The escape lemma for geodesics

At a finite endpoint of its maximal interval, a maximal geodesic leaves every compact subset of the manifold. A maximal geodesic travels at constant speed, so its velocity lift stays among the tangent vectors of norm at most the initial speed. Over a compact subset of the manifold these vectors form a compact subset of the tangent bundle, and an integral curve of the geodesic spray cannot remain in a compact set as it approaches a finite endpoint of its maximal interval.

The step about velocities is not implicit in constant speed: that bounds the velocity in the fibrewise Riemannian norm, and it is the compactness of the norm-bounded part of a Riemannian bundle over a compact set which converts such a bound into relative compactness in the total space.

The escape lemma shows that metric completeness implies geodesic completeness, and it computes maximal geodesic intervals in examples: a geodesic that stays in a compact set up to a finite time is still defined at that time.

Main results

• TauCeti.Manifold.eventually_notMem_nhdsLT_maximalGeodesic: the escape lemma at a finite right endpoint of the maximal interval.
• TauCeti.Manifold.eventually_notMem_nhdsGT_maximalGeodesic: the escape lemma at a finite left endpoint.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer, 2013, Lemma 9.19 (the escape lemma for integral curves).
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6 (its use in the Hopf–Rinow theorem).

theorem TauCeti.Manifold.eventually_notMem_nhdsLT_maximalGeodesic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {v : TangentSpace I p} {b : ℝ} (hb : IsLUB (geodesicInterval I M p v) b) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin b (Set.Iio b), maximalGeodesic I M p v t ∉ K

The escape lemma for geodesics at a finite right endpoint. If the maximal interval of the geodesic with initial data (p, v) is bounded above, with least upper bound b, the maximal geodesic leaves every compact set as t → b⁻.

theorem TauCeti.Manifold.eventually_notMem_nhdsGT_maximalGeodesic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {v : TangentSpace I p} {a : ℝ} (ha : IsGLB (geodesicInterval I M p v) a) {K : Set M} (hK : IsCompact K) : ∀ᶠ (t : ℝ) in nhdsWithin a (Set.Ioi a), maximalGeodesic I M p v t ∉ K

The escape lemma for geodesics at a finite left endpoint. If the maximal interval of the geodesic with initial data (p, v) is bounded below, with greatest lower bound a, the maximal geodesic leaves every compact set as t → a⁺.