Maximal intervals of geodesics

For initial data (p, v), this file defines the set of times covered by open intervals carrying geodesic witnesses with those initial data and proves that it is an open interval in ℝ. On a boundaryless manifold, it proves local existence, uniqueness on overlapping intervals, and that this interval contains zero. The key homogeneity theorem identifies the interval for a • v with the inverse scalar image of the interval for v; this is the domain statement used later by the exponential map.

The interval is defined as a union of geodesic witnesses, so the definition itself does not choose one geodesic on the union. Its membership characterization is suitable for downstream arguments that need an actual witness; a chosen maximal curve and finite-endpoint extension are separate results.

Main definitions and results

• TauCeti.Manifold.geodesicInterval is the maximal interval of geodesic existence.
• TauCeti.Manifold.exists_geodesicCurveOnFrom_Ioo gives local geodesic existence on a boundaryless manifold.
• TauCeti.Manifold.isOpen_geodesicInterval and TauCeti.Manifold.ordConnected_geodesicInterval give its interval structure.
• TauCeti.Manifold.mem_geodesicInterval_iff extracts a geodesic witness from membership.
• TauCeti.Manifold.IsGeodesicCurveOn.sub_mem_geodesicInterval: for a geodesic γ on an open interval and interior parameters τ, t, the time t - τ lies in the maximal interval with initial data (γ τ, γ'(τ)).
• TauCeti.Manifold.IsGeodesicCurveOnFrom.eqOn_of_inter gives uniqueness on overlapping intervals for a boundaryless Hausdorff manifold.
• TauCeti.Manifold.mem_geodesicInterval_smul_iff is the precise nonzero scalar domain relation.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §2.
• J. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 5.

theorem TauCeti.Manifold.exists_geodesicCurveOnFrom {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] (p : M) (v : TangentSpace I p) : ∃ s ∈ nhds 0, ∃ (γ : ℝ → M), IsGeodesicCurveOnFrom I γ s p v

A smooth boundaryless Riemannian manifold has a geodesic with any prescribed initial data on a neighbourhood of the initial parameter.

theorem TauCeti.Manifold.exists_geodesicCurveOnFrom_Ioo {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] (p : M) (v : TangentSpace I p) : ∃ (a : ℝ) (b : ℝ), a < b ∧ 0 ∈ Set.Ioo a b ∧ ∃ (γ : ℝ → M), IsGeodesicCurveOnFrom I γ (Set.Ioo a b) p v

On a boundaryless manifold, a neighbourhood of zero contains an interval of geodesic existence.

The maximal interval

def TauCeti.Manifold.geodesicInterval {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] [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) : Set ℝ

The union of times covered by open-interval geodesic witnesses with initial data (p, v).

theorem TauCeti.Manifold.mem_geodesicInterval_iff {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] [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 : ℝ} : t ∈ geodesicInterval I M p v ↔ ∃ (γ : ℝ → M) (a : ℝ) (b : ℝ), IsGeodesicCurveOnFrom I γ (Set.Ioo a b) p v ∧ t ∈ Set.Ioo a b

Membership in geodesicInterval is witnessed by a geodesic on an open interval containing the given time.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.subset_geodesicInterval {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] [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} {γ : ℝ → M} {a b : ℝ} (h : IsGeodesicCurveOnFrom I γ (Set.Ioo a b) p v) : Set.Ioo a b ⊆ geodesicInterval I M p v

Every geodesic witness with initial data (p, v) is defined inside geodesicInterval I M p v.

theorem TauCeti.Manifold.IsGeodesicCurveOn.sub_mem_geodesicInterval {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {γ : ℝ → M} {a b τ t : ℝ} (hγ : IsGeodesicCurveOn I γ (Set.Ioo a b)) (hτ : τ ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b) : t - τ ∈ geodesicInterval I M (γ τ) (curveVelocity I γ τ)

For a geodesic γ on an open interval (a, b) and τ, t ∈ (a, b), the time t - τ lies in the maximal interval of the geodesic with initial data (γ τ, γ'(τ)).

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.eqOn_of_inter {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] {p : M} {v : TangentSpace I p} {γ γ' : ℝ → M} {a b a' b' : ℝ} (hγ : IsGeodesicCurveOnFrom I γ (Set.Ioo a b) p v) (hγ' : IsGeodesicCurveOnFrom I γ' (Set.Ioo a' b') p v) : Set.EqOn γ γ' (Set.Ioo (max a a') (min b b'))

Geodesics with the same initial data agree on the overlap of their intervals.

theorem TauCeti.Manifold.isOpen_geodesicInterval {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] [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} : IsOpen (geodesicInterval I M p v)

The maximal geodesic interval is open.

theorem TauCeti.Manifold.ordConnected_geodesicInterval {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] [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} : (geodesicInterval I M p v).OrdConnected

The maximal geodesic interval is order-connected, hence an interval in ℝ.

theorem TauCeti.Manifold.isPreconnected_geodesicInterval {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] [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} : IsPreconnected (geodesicInterval I M p v)

The maximal geodesic interval is preconnected.

theorem TauCeti.Manifold.zero_mem_geodesicInterval_of_mem {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] [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 : ℝ} (h : t ∈ geodesicInterval I M p v) : 0 ∈ geodesicInterval I M p v

A nonempty maximal geodesic interval contains the initial parameter: any geodesic witness is defined on an open interval around 0. Unlike zero_mem_geodesicInterval, this needs no boundarylessness.

@[simp]

theorem TauCeti.Manifold.zero_mem_geodesicInterval {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] {p : M} {v : TangentSpace I p} : 0 ∈ geodesicInterval I M p v

On a boundaryless manifold, the initial parameter belongs to the maximal geodesic interval.

@[simp]

theorem TauCeti.Manifold.geodesicInterval_zero {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {p : M} : geodesicInterval I M p 0 = Set.univ

The zero-velocity geodesic exists for all time.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.exists_comp_mul_left_Ioo {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] [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} {γ : ℝ → M} {b c : ℝ} (hγ : IsGeodesicCurveOnFrom I γ (Set.Ioo b c) p v) {a : ℝ} (ha : a ≠ 0) : ∃ (d : ℝ) (e : ℝ), (fun (s : ℝ) => a * s) ⁻¹' Set.Ioo b c = Set.Ioo d e ∧ IsGeodesicCurveOnFrom I (γ ∘ fun (s : ℝ) => a * s) (Set.Ioo d e) p (a • v)

A nonzero linear rescaling of the parameter transforms an open-interval geodesic witness into another open-interval witness. The new interval is the inverse image of the old one.

@[simp]

theorem TauCeti.Manifold.mem_geodesicInterval_smul_iff {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] [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} {a t : ℝ} (ha : a ≠ 0) : t ∈ geodesicInterval I M p (a • v) ↔ a * t ∈ geodesicInterval I M p v

Nonzero rescaling of the initial velocity rescales the maximal interval by the inverse.