The maximal geodesic with prescribed initial data

This file turns the maximal-interval description of geodesic existence into a canonical curve. The maximal geodesic through p with initial velocity v is the base projection of the maximal integral curve of the geodesic spray through (p, v). Its integral-curve domain is proved to be exactly geodesicInterval I M p v, so the projected curve is a geodesic with the prescribed initial data on the whole of that interval.

The definition is total and takes the value p outside its natural domain. Mathematical uses of the curve therefore carry membership in geodesicInterval; this is the domain discipline needed to define the Riemannian exponential map by evaluation at time one.

Main definitions and results

• TauCeti.Manifold.maximalGeodesic is the chosen maximal geodesic with prescribed initial data.
• TauCeti.Manifold.maximalGeodesic_def identifies it with the base projection of the maximal integral curve of the geodesic spray.
• TauCeti.Manifold.maximalIntegralCurveInterval_geodesicSpray identifies the two independently defined maximal domains.
• TauCeti.Manifold.isGeodesicCurveOnFrom_maximalGeodesic gives the geodesic equation and initial data on the maximal domain.
• TauCeti.Manifold.IsGeodesicCurveOnFrom.eqOn_maximalGeodesic is the corresponding uniqueness theorem for any open-interval geodesic witness.
• TauCeti.Manifold.IsGeodesicCurveOnFrom.eq_maximalGeodesic_of_univ specializes uniqueness to geodesics defined for all time.
• TauCeti.Manifold.IsGeodesicCurveOn.maximalGeodesic_sub_eq: a geodesic γ on an open interval is a translate of a piece of the maximal geodesic with initial data (γ τ, γ'(τ)), for any interior parameter τ.
• TauCeti.Manifold.maximalGeodesic_smul is homogeneity in the initial velocity and time.
• TauCeti.Manifold.maximalIntegralCurve_geodesicSpray identifies the maximal integral curve of the geodesic spray with the velocity lift of the maximal geodesic.
• TauCeti.Manifold.maximalGeodesic_add and TauCeti.Manifold.mem_geodesicInterval_maximalGeodesic_iff are the flow law: restarting the maximal geodesic at time t from the point and velocity it has there translates both the curve and its maximal interval by t.
• TauCeti.Manifold.acceleration_maximalGeodesic_eq_zero is the geodesic equation: the unrestricted covariant acceleration of the maximal geodesic vanishes on its maximal interval.

References

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

noncomputable def TauCeti.Manifold.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] [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 : ℝ) : M

The maximal geodesic through p with initial velocity v, junk-valued at p outside its maximal interval.

theorem TauCeti.Manifold.maximalGeodesic_def {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 : ℝ) : maximalGeodesic I M p v t = (maximalIntegralCurve (geodesicSpray I M) ⟨p, v⟩ t).proj

The maximal geodesic is the base projection of the corresponding maximal integral curve of the geodesic spray.

theorem TauCeti.Manifold.maximalIntegralCurveInterval_geodesicSpray {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) : maximalIntegralCurveInterval (geodesicSpray I M) ⟨p, v⟩ = geodesicInterval I M p v

The maximal integral-curve domain of the geodesic spray through (p, v) is the maximal geodesic interval with initial data (p, v).

theorem TauCeti.Manifold.exists_Ioo_subset_geodesicInterval_of_isLUB {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} {b : ℝ} (hb : IsLUB (geodesicInterval I M p v) b) : ∃ a < 0, 0 < b ∧ Set.Ioo a b ⊆ geodesicInterval I M p v

The maximal geodesic interval contains an open interval with the same right endpoint and a negative left endpoint. In particular a finite least upper bound of the interval is positive.

theorem TauCeti.Manifold.exists_Ioo_subset_geodesicInterval_of_isGLB {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 : ℝ} (ha : IsGLB (geodesicInterval I M p v) a) : ∃ b > 0, a < 0 ∧ Set.Ioo a b ⊆ geodesicInterval I M p v

The maximal geodesic interval contains an open interval with the same left endpoint and a positive right endpoint. In particular a finite greatest lower bound of the interval is negative.

@[simp]

theorem TauCeti.Manifold.maximalGeodesic_eq_of_not_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] [I.Boundaryless] {p : M} {v : TangentSpace I p} {t : ℝ} (ht : t ∉ geodesicInterval I M p v) : maximalGeodesic I M p v t = p

Outside its maximal interval, the total maximal geodesic takes its junk value p.

theorem TauCeti.Manifold.isGeodesicCurveOnFrom_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] [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) : IsGeodesicCurveOnFrom I (maximalGeodesic I M p v) (geodesicInterval I M p v) p v

The maximal geodesic has the prescribed initial data on its maximal interval.

@[simp]

theorem TauCeti.Manifold.maximalGeodesic_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) (v : TangentSpace I p) : maximalGeodesic I M p v 0 = p

The maximal geodesic starts at its prescribed base point.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.eqOn_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] [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 : ℝ} (hγ : IsGeodesicCurveOnFrom I γ (Set.Ioo a b) p v) : Set.EqOn (maximalGeodesic I M p v) γ (Set.Ioo a b)

Every geodesic with initial data (p, v) on an open interval around zero agrees there with the maximal geodesic.

theorem TauCeti.Manifold.IsGeodesicCurveOnFrom.eq_maximalGeodesic_of_univ {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} (hγ : IsGeodesicCurveOnFrom I γ Set.univ p v) (t : ℝ) : maximalGeodesic I M p v t = γ t

A geodesic defined for all time with initial data (p, v) is the maximal geodesic.

theorem TauCeti.Manifold.IsGeodesicCurveOn.maximalGeodesic_sub_eq {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] {γ : ℝ → M} {a b τ t : ℝ} (hγ : IsGeodesicCurveOn I γ (Set.Ioo a b)) (hτ : τ ∈ Set.Ioo a b) (ht : t ∈ Set.Ioo a b) : maximalGeodesic I M (γ τ) (curveVelocity I γ τ) (t - τ) = γ t

A geodesic is a translate of a piece of a maximal geodesic. For a geodesic γ on an open interval (a, b) and τ, t ∈ (a, b), the maximal geodesic with initial data (γ τ, γ'(τ)) takes the value γ t at time t - τ.

@[simp]

theorem TauCeti.Manifold.maximalGeodesic_zero_velocity {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) : maximalGeodesic I M p 0 = fun (x : ℝ) => p

The maximal geodesic with zero initial velocity is the constant curve.

@[simp]

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

Rescaling the initial velocity rescales time along the maximal geodesic, whenever the displayed time belongs to the corresponding maximal interval.

theorem TauCeti.Manifold.maximalIntegralCurve_geodesicSpray {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} {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : maximalIntegralCurve (geodesicSpray I M) ⟨p, v⟩ t = ⟨maximalGeodesic I M p v t, curveVelocityWithin I (maximalGeodesic I M p v) (geodesicInterval I M p v) t⟩

At every parameter of its maximal interval, the maximal integral curve of the geodesic spray through (p, v) is the velocity lift of the maximal geodesic.

theorem TauCeti.Manifold.maximalGeodesic_add {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} {t s : ℝ} (ht : t ∈ geodesicInterval I M p v) (hts : t + s ∈ geodesicInterval I M p v) : maximalGeodesic I M p v (t + s) = maximalGeodesic I M (maximalGeodesic I M p v t) (curveVelocityWithin I (maximalGeodesic I M p v) (geodesicInterval I M p v) t) s

The flow law for maximal geodesics. Restarting the maximal geodesic from p with initial velocity v at a time t of its maximal interval, from the point and velocity it has there, and running it for time s gives its value at time t + s, whenever t + s also lies in the maximal interval.

@[simp]

theorem TauCeti.Manifold.mem_geodesicInterval_maximalGeodesic_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] [I.Boundaryless] [T2Space M] {p : M} {v : TangentSpace I p} {t s : ℝ} (ht : t ∈ geodesicInterval I M p v) : s ∈ geodesicInterval I M (maximalGeodesic I M p v t) (curveVelocityWithin I (maximalGeodesic I M p v) (geodesicInterval I M p v) t) ↔ t + s ∈ geodesicInterval I M p v

The maximal interval after restarting a maximal geodesic. Restarting the maximal geodesic from p with initial velocity v at a time t of its maximal interval, from the point and velocity it has there, translates the maximal interval by -t.

theorem TauCeti.Manifold.acceleration_maximalGeodesic_eq_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] [I.Boundaryless] [T2Space M] {p : M} {v : TangentSpace I p} {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : (CovariantDerivative.leviCivitaConnection I M).acceleration (maximalGeodesic I M p v) t = 0

The unrestricted covariant acceleration of a maximal geodesic vanishes at every point of its maximal interval.