Length of geodesics

A geodesic has constant speed on a preconnected parameter set, so its directed Riemannian length from parameter s to t is its speed times ENNReal.ofReal (t - s); the length is zero when t < s. For maximal geodesics this gives the Lipschitz bound used in the metric-completeness argument for geodesic completeness.

Main results

• TauCeti.Manifold.IsGeodesicCurveOn.pathELength_eq: on a preconnected parameter set, the directed length of a geodesic is its speed times the elapsed time.
• TauCeti.Manifold.norm_curveVelocityWithin_maximalGeodesic: the velocity of a maximal geodesic has the norm of its initial velocity throughout its interval.
• TauCeti.Manifold.pathELength_maximalGeodesic: its directed length from s to t is its initial speed times ENNReal.ofReal (t - s).

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6.

theorem TauCeti.Manifold.IsGeodesicCurveOn.pathELength_eq {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s : Set ℝ} (h : IsGeodesicCurveOn I γ s) (hconn : IsPreconnected s) {a b c : ℝ} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : Manifold.pathELength I γ a b = ‖curveVelocityWithin I γ s c‖ₑ * ENNReal.ofReal (b - a)

On an interval with endpoints in its preconnected domain, the directed length of a geodesic from a to b is its speed at any chosen time in that domain times ENNReal.ofReal (b - a). The domain need not be open, so this applies to geodesic segments on closed intervals.

theorem TauCeti.Manifold.norm_curveVelocityWithin_maximalGeodesic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {v : TangentSpace I p} {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : ‖curveVelocityWithin I (maximalGeodesic I M p v) (geodesicInterval I M p v) t‖ = ‖v‖

At every parameter of its maximal interval, the maximal geodesic from p with initial velocity v has velocity of norm ‖v‖.

theorem TauCeti.Manifold.pathELength_maximalGeodesic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {v : TangentSpace I p} {s t : ℝ} (hs : s ∈ geodesicInterval I M p v) (ht : t ∈ geodesicInterval I M p v) : Manifold.pathELength I (maximalGeodesic I M p v) s t = ‖v‖ₑ * ENNReal.ofReal (t - s)

The directed length from s to t of the maximal geodesic from p with initial velocity v is ‖v‖ * ENNReal.ofReal (t - s), and hence is zero when t < s.