Constant speed of geodesics

A geodesic has constant speed on every preconnected parameter set, and hence on each connected component of an arbitrary parameter set. We first prove that the inner product of its within-set velocity with itself is constant, by differentiating it with the within-set metric-product rule and using the geodesic equation. Taking square roots gives the usual constant-speed statement. On an open set this velocity agrees with the unrestricted curveVelocity by curveVelocityWithin_of_mem_nhds; the all-time specializations below are stated directly with curveVelocity.

Main results

• TauCeti.Manifold.IsGeodesicCurveOn.inner_curveVelocityWithin_self_eq: squared speed is constant on a preconnected parameter set.
• TauCeti.Manifold.IsGeodesicCurveOn.norm_curveVelocityWithin_eq: speed is constant there.
• TauCeti.Manifold.IsGeodesicCurveOn.inner_curveVelocityWithin_self_eq_of_mem_connectedComponentIn and TauCeti.Manifold.IsGeodesicCurveOn.norm_curveVelocityWithin_eq_of_mem_connectedComponentIn: on an arbitrary parameter set, squared speed and speed are constant on each connected component.
• TauCeti.Manifold.IsGeodesicCurveOn.energy_eq: the energy of a geodesic segment is (b - a) ‖curveVelocityWithin I γ s a‖² / 2, on any parameter set s containing the segment.
• TauCeti.Manifold.IsGeodesicCurve.inner_curveVelocity_self_eq: an all-time geodesic has the same squared speed at any two parameters.
• TauCeti.Manifold.IsGeodesicCurve.norm_curveVelocity_eq: an all-time geodesic has the same speed at any two parameters.
• TauCeti.Manifold.IsGeodesicCurve.energy_eq: the energy of an all-time geodesic between a and b is (b - a) ‖curveVelocity I γ a‖² / 2.
• TauCeti.Manifold.inner_curveVelocity_maximalGeodesic_self: the squared speed of a maximal geodesic is that of its initial velocity.
• TauCeti.Manifold.energy_maximalGeodesic: hence its energy between two parameters of its maximal interval is (b - a) ‖v‖² / 2.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 3, §2.
• The proof follows the organization of DoCarmoLib/Riemannian/Geodesic/HopfRinow/ConstantSpeed.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, using Tau Ceti's set-aware geodesic predicate and Mathlib's Riemannian norm.

theorem TauCeti.Manifold.IsGeodesicCurveOn.inner_curveVelocityWithin_self_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 : ℝ} (ha : a ∈ s) (hb : b ∈ s) : inner ℝ (curveVelocityWithin I γ s a) (curveVelocityWithin I γ s a) = inner ℝ (curveVelocityWithin I γ s b) (curveVelocityWithin I γ s b)

Squared speed is constant along a geodesic. On a preconnected parameter set, the inner product of the within-set velocity with itself has the same value at every two parameters. On an open set this velocity agrees with the unrestricted curveVelocity by curveVelocityWithin_of_mem_nhds.

theorem TauCeti.Manifold.IsGeodesicCurveOn.norm_curveVelocityWithin_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 : ℝ} (ha : a ∈ s) (hb : b ∈ s) : ‖curveVelocityWithin I γ s a‖ = ‖curveVelocityWithin I γ s b‖

A geodesic has constant speed. On a preconnected parameter set, the norm of its within-set velocity has the same value at every two parameters. On an open set this velocity agrees with the unrestricted curveVelocity by curveVelocityWithin_of_mem_nhds.

theorem TauCeti.Manifold.IsGeodesicCurveOn.inner_curveVelocityWithin_self_eq_of_mem_connectedComponentIn {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) {a b : ℝ} (hb : b ∈ connectedComponentIn s a) : inner ℝ (curveVelocityWithin I γ s a) (curveVelocityWithin I γ s a) = inner ℝ (curveVelocityWithin I γ s b) (curveVelocityWithin I γ s b)

Squared speed is constant on each connected component of the parameter set: without preconnectedness, two parameters in the same connected component of s give the within-set velocity the same inner product with itself.

theorem TauCeti.Manifold.IsGeodesicCurveOn.norm_curveVelocityWithin_eq_of_mem_connectedComponentIn {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) {a b : ℝ} (hb : b ∈ connectedComponentIn s a) : ‖curveVelocityWithin I γ s a‖ = ‖curveVelocityWithin I γ s b‖

A geodesic has constant speed on each connected component of its parameter set: two parameters in the same connected component of s give within-set velocities of the same norm.

theorem TauCeti.Manifold.IsGeodesicCurveOn.energy_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) {a b : ℝ} (hsub : Set.uIcc a b ⊆ s) : energy I γ a b = (b - a) * ‖curveVelocityWithin I γ s a‖ ^ 2 / 2

The energy of a geodesic segment. A geodesic has constant speed, so its energy between a and b is (b - a) ‖curveVelocityWithin I γ s a‖² / 2 whenever the parameter set s contains the interval between them. The speed is that of the within-set velocity, so s need not be open: this applies to geodesic segments on closed intervals.

theorem TauCeti.Manifold.IsGeodesicCurve.inner_curveVelocity_self_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} (h : IsGeodesicCurve I γ) (a b : ℝ) : inner ℝ (curveVelocity I γ a) (curveVelocity I γ a) = inner ℝ (curveVelocity I γ b) (curveVelocity I γ b)

An all-time geodesic has the same squared speed, expressed using the unrestricted curveVelocity, at every two parameters.

theorem TauCeti.Manifold.IsGeodesicCurve.norm_curveVelocity_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} (h : IsGeodesicCurve I γ) (a b : ℝ) : ‖curveVelocity I γ a‖ = ‖curveVelocity I γ b‖

An all-time geodesic has the same speed, expressed using the unrestricted curveVelocity, at every two parameters.

theorem TauCeti.Manifold.IsGeodesicCurve.energy_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} (h : IsGeodesicCurve I γ) (a b : ℝ) : energy I γ a b = (b - a) * ‖curveVelocity I γ a‖ ^ 2 / 2

The energy of an all-time geodesic between a and b is (b - a) ‖γ'(a)‖² / 2, expressed using the unrestricted curveVelocity.

theorem TauCeti.Manifold.inner_curveVelocity_maximalGeodesic_self {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} {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : inner ℝ (curveVelocity I (maximalGeodesic I M p v) t) (curveVelocity I (maximalGeodesic I M p v) t) = inner ℝ v v

The squared speed of a maximal geodesic equals the squared norm of its initial velocity at every point of its maximal interval.

theorem TauCeti.Manifold.energy_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 b : ℝ} (ha : a ∈ geodesicInterval I M p v) (hb : b ∈ geodesicInterval I M p v) : energy I (maximalGeodesic I M p v) a b = (b - a) * ‖v‖ ^ 2 / 2

On any subinterval of its maximal interval, the energy of a maximal geodesic is half the squared norm of its initial velocity times the duration.