Restriction and affine reparametrization of geodesics

A geodesic remains a geodesic after restricting its parameter set, provided the smaller set still has unique derivatives. It also remains a geodesic after an affine change of parameter t ↦ a * t + b. The latter statement is special to affine reparametrizations: the velocity gains one factor of a, and its covariant derivative gains a second factor, with no acceleration term from the reparametrization.

The proofs use the naturality of CovariantDerivative.alongCurveWithin and the C¹ regularity of the coordinate reading of the velocity of a C² curve. Every domain condition is explicit: restriction needs an inclusion of parameter sets, while reparametrization needs the affine map to carry the new parameter set into the old one. Restriction is the case a = 1, b = 0 of the affine statement.

The same two operations are recorded for geodesics carrying prescribed initial data: restriction to a parameter set still containing 0 keeps the initial data, and the scaling t ↦ a * t, which fixes 0, keeps the initial point and multiplies the initial velocity by a. Conversely, a geodesic on an open interval acquires initial data once an interior parameter τ is translated to 0: its initial data are then (γ τ, γ'(τ)).

Main results

• TauCeti.Manifold.IsGeodesicCurveOn.comp_affine: precompose a geodesic with t ↦ a * t + b.
• TauCeti.Manifold.IsGeodesicCurveOn.mono: restrict a geodesic to a smaller parameter set.
• TauCeti.Manifold.IsGeodesicCurve.comp_affine: the all-time specialization.
• TauCeti.Manifold.IsGeodesicCurveOnFrom.mono and TauCeti.Manifold.IsGeodesicCurveOnFrom.comp_mul_left: the two operations on a geodesic with prescribed initial data.
• TauCeti.Manifold.IsGeodesicCurveOn.isGeodesicCurveOnFrom_comp_add_const: translating a geodesic on an open interval so that an interior parameter τ becomes 0 gives a geodesic with initial data (γ τ, γ'(τ)).

References

• M. P. do Carmo, Riemannian Geometry, Chapter 3, Section 2.
• J. M. Lee, Introduction to Riemannian Manifolds, Chapter 4, Problem 4-10.
• The reparametrization argument follows ParallelReparametrization.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, adapted to Tau Ceti's interval-aware geodesic and along-curve APIs.

theorem TauCeti.Manifold.IsGeodesicCurveOn.comp_affine {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s u : Set ℝ} (h : IsGeodesicCurveOn I γ s) (a b : ℝ) (hu : UniqueDiffOn ℝ u) (hmaps : Set.MapsTo (fun (t : ℝ) => a * t + b) u s) : IsGeodesicCurveOn I (γ ∘ fun (t : ℝ) => a * t + b) u

A geodesic remains a geodesic after the affine reparametrization t ↦ a * t + b, provided that map carries the new parameter set into the original one. The case a = 0 is included and gives a constant curve.

theorem TauCeti.Manifold.IsGeodesicCurveOn.mono {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s u : Set ℝ} (h : IsGeodesicCurveOn I γ s) (hu : UniqueDiffOn ℝ u) (hus : u ⊆ s) : IsGeodesicCurveOn I γ u

A geodesic remains a geodesic after restriction to a smaller parameter set with unique derivatives. The smaller set need not be open or an interval.

theorem TauCeti.Manifold.IsGeodesicCurve.comp_affine {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} (h : IsGeodesicCurve I γ) (a b : ℝ) : IsGeodesicCurve I (γ ∘ fun (t : ℝ) => a * t + b)

An all-time geodesic remains an all-time geodesic after an affine reparametrization.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.mono {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s u : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) (hu : UniqueDiffOn ℝ u) (hus : u ⊆ s) (h0 : 0 ∈ u) : IsGeodesicCurveOnFrom I γ u p v

A geodesic with prescribed initial data keeps that data after restriction to a smaller parameter set with unique derivatives which still contains the initial parameter 0.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.comp_mul_left {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {s u : Set ℝ} {p : M} {v : TangentSpace I p} (h : IsGeodesicCurveOnFrom I γ s p v) (a : ℝ) (hu : UniqueDiffOn ℝ u) (hmaps : Set.MapsTo (fun (t : ℝ) => a * t) u s) (h0 : 0 ∈ u) : IsGeodesicCurveOnFrom I (γ ∘ fun (t : ℝ) => a * t) u p (a • v)

The reparametrization t ↦ a * t fixes the initial parameter 0, so a geodesic with prescribed initial data keeps its initial point and has its initial velocity multiplied by a.

theorem TauCeti.Manifold.IsGeodesicCurveOn.isGeodesicCurveOnFrom_comp_add_const {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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b τ : ℝ} (hγ : IsGeodesicCurveOn I γ (Set.Ioo a b)) (hτ : τ ∈ Set.Ioo a b) : IsGeodesicCurveOnFrom I (γ ∘ fun (u : ℝ) => u + τ) (Set.Ioo (a - τ) (b - τ)) (γ τ) (curveVelocity I γ τ)

Restarting a geodesic. Translating a geodesic γ on an open interval (a, b) in time, so that a parameter τ ∈ (a, b) becomes 0, gives a geodesic on (a - τ, b - τ) with initial data (γ τ, γ'(τ)).