The smooth geodesic flow

The geodesic spray of a smooth finite-dimensional Riemannian manifold has a family of integral curves depending smoothly on the initial tangent vector and on time. Projecting each spray trajectory to the manifold gives the geodesic with that initial position and velocity, on one common open time neighbourhood for all nearby initial data.

Globally, the maximal integral curves of the spray form the geodesic flow on the tangent bundle. Its natural domain is the set of pairs (z, t) of a tangent vector z ∈ T_x M and a time t in the maximal geodesic interval of z; this domain is open, the flow is jointly smooth on it, and so is its base projection, the maximal geodesic regarded as a function of its initial data and time. This is the smooth-dependence input for smoothness of the exponential map on its natural domain.

Main results

• TauCeti.Manifold.exists_contMDiffAt_localGeodesicFlow: local spray trajectories form a jointly smooth family, and their base projections have the prescribed geodesic initial data.
• TauCeti.Manifold.maximalIntegralCurveFlowDomain_geodesicSpray: the domain of the geodesic flow consists of the pairs (z, t) with t in the maximal geodesic interval of z.
• TauCeti.Manifold.isOpen_setOfPred_mem_geodesicInterval: this domain is open in TM × ℝ.
• TauCeti.Manifold.contMDiffOn_maximalIntegralCurve_geodesicSpray: the maximal geodesic flow is smooth on its domain.
• TauCeti.Manifold.contMDiffOn_maximalGeodesic: maximal geodesics depend smoothly on their initial data and on time.
• TauCeti.Manifold.contMDiffAt_maximalGeodesic_comp: a curve of initial states gives a jointly Cⁿ geodesic variation at each point of the central maximal interval.
• TangentBundle.exists_contMDiffOn_maximalGeodesic_of_isCompact: nearby initial states share a smooth flow domain around any compact subset of a maximal geodesic interval.
• TauCeti.Manifold.exists_contMDiffOn_maximalGeodesic_comp_of_isCompact: a curve of initial states gives a geodesic variation on a common domain around a compact time subset.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 3, §2.
• J. M. Lee, Introduction to Riemannian Manifolds, Chapter 5.

theorem TauCeti.Manifold.exists_contMDiffAt_localGeodesicFlow {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (z : TangentBundle I M) : ∃ U ∈ nhds z, ∃ s ∈ nhds 0, IsOpen s ∧ ∃ (Φ : TangentBundle I M → ℝ → TangentBundle I M), ContMDiffAt (I.tangent.prod (modelWithCornersSelf ℝ ℝ)) I.tangent (↑⊤) (fun (p : TangentBundle I M × ℝ) => Φ p.1 p.2) (z, 0) ∧ ∀ w ∈ U, Φ w 0 = w ∧ IsMIntegralCurveOn (Φ w) (geodesicSpray I M) s ∧ (∀ t ∈ s, ∀ (u : ℝ), Φ w (t + u) = Φ (Φ w t) u) ∧ IsGeodesicCurveOnFrom I (fun (t : ℝ) => (Φ w t).proj) s w.proj w.snd

The smooth local geodesic flow. Near every initial state z : TM, the integral curves of the geodesic spray exist on a common open time neighbourhood and depend smoothly on the initial state and time at (z, 0). Their base projections are geodesics with the position and velocity encoded by each nearby initial state.

The maximal geodesic flow

theorem TauCeti.Manifold.maximalIntegralCurveFlowDomain_geodesicSpray {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] : maximalIntegralCurveFlowDomain (geodesicSpray I M) = {q : TangentBundle I M × ℝ | q.2 ∈ geodesicInterval I M q.1.proj q.1.snd}

The domain of the maximal flow of the geodesic spray consists of the pairs (z, t) for which t lies in the maximal geodesic interval of the initial data encoded by z.

theorem TauCeti.Manifold.isOpen_setOfPred_mem_geodesicInterval {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] : IsOpen {q : TangentBundle I M × ℝ | q.2 ∈ geodesicInterval I M q.1.proj q.1.snd}

The domain of the geodesic flow is open: the pairs (z, t) of a tangent vector and a time of its maximal geodesic interval form an open subset of TM × ℝ.

theorem TauCeti.Manifold.contMDiffOn_maximalIntegralCurve_geodesicSpray {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] : ContMDiffOn (I.tangent.prod (modelWithCornersSelf ℝ ℝ)) I.tangent (↑⊤) (fun (q : TangentBundle I M × ℝ) => maximalIntegralCurve (geodesicSpray I M) q.1 q.2) {q : TangentBundle I M × ℝ | q.2 ∈ geodesicInterval I M q.1.proj q.1.snd}

The maximal geodesic flow is smooth. The maximal integral curves of the geodesic spray depend smoothly, jointly in the initial tangent vector and in time, on the domain of the geodesic flow.

theorem TauCeti.Manifold.contMDiffOn_maximalGeodesic {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] : ContMDiffOn (I.tangent.prod (modelWithCornersSelf ℝ ℝ)) I (↑⊤) (fun (q : TangentBundle I M × ℝ) => maximalGeodesic I M q.1.proj q.1.snd q.2) {q : TangentBundle I M × ℝ | q.2 ∈ geodesicInterval I M q.1.proj q.1.snd}

Smooth dependence of maximal geodesics on initial data. The maximal geodesic with initial point z.proj and initial velocity z.2, evaluated at time t, is a smooth function of (z, t) on the domain of the geodesic flow.

theorem TauCeti.Manifold.contMDiffAt_maximalGeodesic_comp {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {σ : ℝ → TangentBundle I M} {n : ℕ} (hσ : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I.tangent (↑n) σ 0) {t : ℝ} (ht : t ∈ geodesicInterval I M (σ 0).proj (σ 0).snd) : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I (↑n) (fun (z : ℝ × ℝ) => maximalGeodesic I M (σ z.1).proj (σ z.1).snd z.2) (0, t)

A Cⁿ curve of initial states gives a jointly Cⁿ geodesic variation at each point of the central maximal geodesic interval, for every finite order n.

theorem TangentBundle.exists_contMDiffOn_maximalGeodesic_of_isCompact {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] (z : TangentBundle I M) {K : Set ℝ} (hK : IsCompact K) (hsub : K ⊆ TauCeti.Manifold.geodesicInterval I M z.proj z.snd) : ∃ (U : Set (TangentBundle I M)) (V : Set ℝ), IsOpen U ∧ IsOpen V ∧ z ∈ U ∧ K ⊆ V ∧ (∀ w ∈ U, V ⊆ TauCeti.Manifold.geodesicInterval I M w.proj w.snd) ∧ ContMDiffOn (I.tangent.prod (modelWithCornersSelf ℝ ℝ)) I (↑⊤) (fun (q : TangentBundle I M × ℝ) => TauCeti.Manifold.maximalGeodesic I M q.1.proj q.1.snd q.2) (U ×ˢ V)

Around a compact subset of a maximal geodesic interval there is one open time domain valid for every nearby initial state, on which the geodesic flow is jointly smooth. In particular a prescribed compact geodesic segment admits variations on a common time domain, even when the metric is incomplete.

theorem TauCeti.Manifold.exists_contMDiffOn_maximalGeodesic_comp_of_isCompact {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] [I.Boundaryless] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {σ : ℝ → TangentBundle I M} {n : ℕ∞} (hσ : ∀ᶠ (q : ℝ) in nhds 0, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I.tangent (↑n) σ q) {K : Set ℝ} (hK : IsCompact K) (hsub : K ⊆ geodesicInterval I M (σ 0).proj (σ 0).snd) : ∃ (U : Set ℝ) (V : Set ℝ), IsOpen U ∧ IsOpen V ∧ 0 ∈ U ∧ K ⊆ V ∧ ContMDiffOn (modelWithCornersSelf ℝ (ℝ × ℝ)) I (↑n) (fun (z : ℝ × ℝ) => maximalGeodesic I M (σ z.1).proj (σ z.1).snd z.2) (U ×ˢ V) ∧ ∀ q ∈ U, IsGeodesicCurveOn I (maximalGeodesic I M (σ q).proj (σ q).snd) V

A Cⁿ curve of initial states gives a Cⁿ geodesic variation on one product neighbourhood of any compact subset of the central maximal interval, including smooth regularity n = ∞. Both the variation parameter and the time domain are open, so derivatives at compact segment endpoints are unrestricted. The initial-state curve is C^n throughout a neighbourhood of zero; for n = ∞, regularity merely at zero would not suffice.