The Riemannian exponential map

For a point p of a smooth finite-dimensional Riemannian manifold M, the exponential map sends a tangent vector v ∈ T_p M to the point reached at time 1 by the maximal geodesic leaving p with velocity v. Its natural domain is the set of v whose maximal geodesic interval contains 1.

The map is defined as a total function which takes the junk value p outside its natural domain; every theorem about its mathematical value carries the corresponding domain hypothesis. The homogeneity of maximal geodesics turns into the two basic facts relating the exponential map to geodesics: t lies in the maximal interval of v exactly when t • v lies in the domain, and then exp_p (t • v) is the maximal geodesic at time t. In particular the domain is star-shaped at 0. Smooth dependence of the maximal geodesic flow shows that the tangent vectors z ∈ T_x M with z in the domain of exp_x form an open subset of the tangent bundle, on which z ↦ exp_x z is smooth, being the geodesic flow at time 1 followed by the base projection. Restricting to the fibre over p, the domain of exp_p is open and exp_p is smooth there. Its differential at the origin is the identity of T_p M, once the tangent space to T_p M at 0 is identified with T_p M itself by NormedSpace.fromTangentSpace; by the inverse function theorem the exponential map is therefore a local diffeomorphism at 0, the input to normal neighbourhoods. Finally, the domain is all of T_p M exactly when every geodesic leaving p is defined for all time.

Main definitions and results

• TauCeti.Manifold.expDomain: the natural domain of the exponential map at p.
• TauCeti.Manifold.riemannianExp: the exponential map at p.
• TauCeti.Manifold.IsGeodesicallyCompleteAt: every geodesic leaving p is defined for all time.
• TauCeti.Manifold.mem_geodesicInterval_iff_smul_mem_expDomain: the maximal interval of v is the set of times t with t • v in the domain.
• TauCeti.Manifold.riemannianExp_smul: exp_p (t • v) is the maximal geodesic at time t, on and off its natural interval (where both sides take the junk value).
• TauCeti.Manifold.mem_expDomain_of_norm_le_dist: a vector with ‖v‖ ≤ dist p (exp_p v) lies in the domain, since off it exp_p v is the junk value p.
• TauCeti.Manifold.starConvex_expDomain: the domain is star-shaped at 0.
• TauCeti.Manifold.isOpen_setOfPred_mem_expDomain and TauCeti.Manifold.contMDiffOn_riemannianExp_tangentBundle: on the tangent bundle, the domain of the exponential map is open and the exponential map is smooth there.
• TauCeti.Manifold.isOpen_expDomain: the natural domain is open.
• TauCeti.Manifold.contMDiffOn_riemannianExp: the exponential map is smooth on its domain.
• TauCeti.Manifold.curveVelocity_riemannianExp_add_smul and TauCeti.Manifold.curveVelocity_riemannianExp_smul: velocities of affine and radial curves through the exponential map.
• TauCeti.Manifold.curveVelocity_riemannianExp_smul_zero: the radial curve s ↦ exp_p (s • v) leaves p with velocity v.
• TauCeti.Manifold.mfderiv_riemannianExp_zero: the differential of the exponential map at 0 is the identity.
• TauCeti.Manifold.isLocalDiffeomorphAt_riemannianExp_zero: the exponential map is a local diffeomorphism at 0.
• TauCeti.Manifold.continuousAt_norm_angular_riemannianExp_zero and TauCeti.Manifold.contDiffOn_inner_angular_riemannianExp: regularity of the differential of the exponential map applied to a fixed tangent vector.
• TauCeti.Manifold.radialVariation_eq_maximalGeodesic, TauCeti.Manifold.contMDiffAt_radialVariation and TauCeti.Manifold.eventually_acceleration_radialVariation_eq_zero: the radial variation exp_p (t • (v + u • w)) is a smooth family of geodesics.
• TauCeti.Manifold.variationField_radialVariation: the variation field of the radial variation is t ↦ d(exp_p)_{t v}(t w).
• TauCeti.Manifold.expDomain_eq_univ_iff: the exponential map at p is defined on all of T_p M exactly when M is geodesically complete at p.

References

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

The domain and the map

def TauCeti.Manifold.expDomain {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) : Set (TangentSpace I p)

The natural domain of the Riemannian exponential map at p: the tangent vectors v whose maximal geodesic from p with initial velocity v is defined at time 1.

noncomputable def TauCeti.Manifold.riemannianExp {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

The Riemannian exponential map at p: the value at time 1 of the maximal geodesic from p with initial velocity v. Outside expDomain I M p it takes the junk value p.

@[simp]

theorem TauCeti.Manifold.mem_expDomain_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} : v ∈ expDomain I M p ↔ 1 ∈ geodesicInterval I M p v

A tangent vector lies in the domain of the exponential map exactly when its maximal geodesic interval contains 1.

theorem TauCeti.Manifold.riemannianExp_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) : riemannianExp I M p v = maximalGeodesic I M p v 1

The exponential map is the maximal geodesic evaluated at time 1.

theorem TauCeti.Manifold.zero_mem_expDomain {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) : 0 ∈ expDomain I M p

The zero vector lies in the domain of the exponential map.

@[simp]

theorem TauCeti.Manifold.riemannianExp_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) : riemannianExp I M p 0 = p

The exponential map sends the zero vector to the base point.

@[simp]

theorem TauCeti.Manifold.riemannianExp_of_notMem_expDomain {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} (hv : v ∉ expDomain I M p) : riemannianExp I M p v = p

Outside its natural domain, the exponential map takes its junk value p.

theorem TauCeti.Manifold.mem_expDomain_of_norm_le_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [I.Boundaryless] {M : Type u_4} [MetricSpace M] [ChartedSpace H M] [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} (hmin : ‖v‖ ≤ dist p (riemannianExp I M p v)) : v ∈ expDomain I M p

A tangent vector v with ‖v‖ ≤ dist p (exp_p v) lies in the domain of exp_p: off the domain exp_p v is the junk value p, which forces v = 0.

Homogeneity

theorem TauCeti.Manifold.mem_geodesicInterval_iff_smul_mem_expDomain {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 : ℝ} : t ∈ geodesicInterval I M p v ↔ t • v ∈ expDomain I M p

The domain of the exponential map along a ray. A time t lies in the maximal geodesic interval of v exactly when t • v lies in the domain of the exponential map.

theorem TauCeti.Manifold.geodesicInterval_eq_preimage_expDomain {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) : geodesicInterval I M p v = (fun (t : ℝ) => t • v) ⁻¹' expDomain I M p

The geodesic interval of v is the preimage of the domain of the exponential map under t ↦ t • v.

theorem TauCeti.Manifold.riemannianExp_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) (t : ℝ) : riemannianExp I M p (t • v) = maximalGeodesic I M p v t

The exponential map along a ray. For every t, the exponential of t • v is the maximal geodesic from p with initial velocity v at time t: on the maximal interval this is the homogeneity of maximal geodesics, while off it both sides take the junk value p.

theorem TauCeti.Manifold.starConvex_expDomain {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) : StarConvex ℝ 0 (expDomain I M p)

The domain of the exponential map is star-shaped at the zero vector.

Regularity

@[instance_reducible]

noncomputable def TauCeti.Manifold.tangentSpaceChartedSpace {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] (p : M) : ChartedSpace (TangentSpace I p) (TangentSpace I p)

Each tangent space is a charted space over itself (via the identity chart), so that smoothness of maps out of a tangent space can be stated in the manifold API.

theorem TauCeti.Manifold.isOpen_setOfPred_mem_expDomain {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] : IsOpen {z : TangentBundle I M | z.snd ∈ expDomain I M z.proj}

The domain of the exponential map in the tangent bundle is open: the tangent vectors z ∈ T_x M lying in the natural domain of exp_x form an open subset of TM.

theorem TauCeti.Manifold.contMDiffOn_riemannianExp_tangentBundle {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] : ContMDiffOn I.tangent I (↑⊤) (fun (z : TangentBundle I M) => riemannianExp I M z.proj z.snd) {z : TangentBundle I M | z.snd ∈ expDomain I M z.proj}

The exponential map is smooth on the tangent bundle. The map z ↦ exp_x z, for z a tangent vector at x, is smooth on the open subset of TM where it is naturally defined: it is the geodesic flow at time 1 followed by the base projection.

theorem TauCeti.Manifold.continuousOn_riemannianExp_tangentBundle {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] : ContinuousOn (fun (z : TangentBundle I M) => riemannianExp I M z.proj z.snd) {z : TangentBundle I M | z.snd ∈ expDomain I M z.proj}

The exponential map is continuous on the open subset of the tangent bundle where it is naturally defined.

theorem TauCeti.Manifold.isOpen_expDomain {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) : IsOpen (expDomain I M p)

The natural domain of the Riemannian exponential map is open.

theorem TauCeti.Manifold.contMDiffOn_riemannianExp {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) : ContMDiffOn (modelWithCornersSelf ℝ (TangentSpace I p)) I (↑⊤) (riemannianExp I M p) (expDomain I M p)

The Riemannian exponential map is smooth on its natural domain.

theorem TauCeti.Manifold.continuousOn_riemannianExp {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) : ContinuousOn (riemannianExp I M p) (expDomain I M p)

The Riemannian exponential map is continuous on its natural domain.

theorem TauCeti.Manifold.contMDiffAt_riemannianExp {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} (hv : v ∈ expDomain I M p) : ContMDiffAt (modelWithCornersSelf ℝ (TangentSpace I p)) I (↑⊤) (riemannianExp I M p) v

The Riemannian exponential map is smooth at every point of its natural domain.

theorem TauCeti.Manifold.curveVelocity_riemannianExp_comp {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} {w : ℝ → TangentSpace I p} {w' : TangentSpace I p} {t : ℝ} (hw : HasDerivAt w w' t) (hwt : w t ∈ expDomain I M p) : curveVelocity I (riemannianExp I M p ∘ w) t = (mfderiv% (riemannianExp I M p) (w t)) w'

The velocity of the exponential image of a path is the differential of the exponential map applied to the derivative of the path in the tangent space.

theorem TauCeti.Manifold.curveVelocity_riemannianExp_add_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 w : TangentSpace I p} {u : ℝ} (hu : v + u • w ∈ expDomain I M p) : curveVelocity I (fun (s : ℝ) => riemannianExp I M p (v + s • w)) u = (mfderiv% (riemannianExp I M p) (v + u • w)) w

The velocity of an affine curve through the exponential map is its differential in the affine direction.

theorem TauCeti.Manifold.curveVelocity_riemannianExp_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} {t : ℝ} (ht : t • v ∈ expDomain I M p) : curveVelocity I (fun (s : ℝ) => riemannianExp I M p (s • v)) t = (mfderiv% (riemannianExp I M p) (t • v)) v

The velocity of a radial curve through the exponential map is its differential in the radial direction.

theorem TauCeti.Manifold.continuousAt_riemannianExp {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} (hv : v ∈ expDomain I M p) : ContinuousAt (riemannianExp I M p) v

The Riemannian exponential map is continuous at every point of its natural domain.

The derivative at the origin

@[simp]

theorem TauCeti.Manifold.mfderiv_riemannianExp_apply_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) : (mfderiv% (riemannianExp I M p) 0) v = v

The differential of the exponential map at the origin sends every tangent vector to itself.

theorem TauCeti.Manifold.contMDiffAt_riemannianExp_smul_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) : ContMDiffAt (modelWithCornersSelf ℝ ℝ) I (↑⊤) (fun (s : ℝ) => riemannianExp I M p (s • v)) 0

The radial curve s ↦ exp_p (s • v) is smooth at time zero.

@[simp]

theorem TauCeti.Manifold.curveVelocity_riemannianExp_smul_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) : curveVelocity I (fun (s : ℝ) => riemannianExp I M p (s • v)) 0 = v

The radial curve s ↦ exp_p (s • v) leaves p with velocity v.

theorem TauCeti.Manifold.mfderiv_riemannianExp_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) : mfderiv% (riemannianExp I M p) 0 = ↑(NormedSpace.fromTangentSpace 0)

The differential of the exponential map at the origin is the identity, under the canonical identification NormedSpace.fromTangentSpace of the tangent space to T_p M at 0 with T_p M.

theorem TauCeti.Manifold.hasMFDerivAt_riemannianExp_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) : HasMFDerivAt% (riemannianExp I M p) 0 ↑(NormedSpace.fromTangentSpace 0)

The exponential map has the identity of T_p M as its derivative at the origin.

theorem TauCeti.Manifold.hasStrictFDerivAt_riemannianExp_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) : HasStrictFDerivAt (writtenInExtChartAt (modelWithCornersSelf ℝ (TangentSpace I p)) I 0 (riemannianExp I M p)) (↑(tangentSpaceCastModel I p)) 0

In extended coordinates, the exponential map has the canonical identification T_p M →L[ℝ] E as its strict derivative at the origin.

theorem TauCeti.Manifold.isLocalDiffeomorphAt_riemannianExp_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) : IsLocalDiffeomorphAt (modelWithCornersSelf ℝ (TangentSpace I p)) I (↑⊤) (riemannianExp I M p) 0

The exponential map is a local diffeomorphism at the origin.

Radial variations

The radial variation F (u, t) = exp_p (t • (v + u • w)) of the geodesic t ↦ exp_p (t • v) is the family of maximal geodesics leaving p with initial velocities v + u • w. Its variation field computes the differential of the exponential map, which is how the Gauss lemma and the identification of that differential with Jacobi fields are proved.

Each statement takes the variation as a function F together with its defining equation, rather than as the explicit two-parameter formula. The fibre in which a velocity vector lives is indexed by the point of the curve, so rewriting a radial curve into the maximal geodesic it equals has to reach the index as well; that is possible for F u and not for the formula, whose index appears already evaluated.

theorem TauCeti.Manifold.radialVariation_eq_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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) (u : ℝ) : F u = maximalGeodesic I M p (v + u • w)

Each radial curve of the variation is the maximal geodesic with the corresponding initial velocity.

theorem TauCeti.Manifold.radialVariation_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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) : F 0 = fun (t : ℝ) => riemannianExp I M p (t • v)

The central curve of the radial variation is the radial geodesic t ↦ exp_p (t • v).

theorem TauCeti.Manifold.radialVariation_apply_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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) (u : ℝ) : F u 0 = p

Every curve of the radial variation starts at p.

theorem TauCeti.Manifold.contMDiffAt_radialVariation {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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) {u t : ℝ} (hut : t • (v + u • w) ∈ expDomain I M p) : ContMDiffAt (modelWithCornersSelf ℝ (ℝ × ℝ)) I (↑⊤) (fun (z : ℝ × ℝ) => F z.1 z.2) (u, t)

The radial variation is smooth at every parameter pair whose radial vector lies in the natural domain of the exponential map.

theorem TauCeti.Manifold.eventually_mem_geodesicInterval_add_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 w : TangentSpace I p} {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : ∀ᶠ (u : ℝ) in nhds 0, t ∈ geodesicInterval I M p (v + u • w)

A parameter of the maximal geodesic interval of v stays in the maximal geodesic interval of v + u • w for all u near 0.

theorem TauCeti.Manifold.acceleration_radialVariation_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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) {u t : ℝ} (ht : t ∈ geodesicInterval I M p (v + u • w)) : (CovariantDerivative.leviCivitaConnection I M).acceleration (F u) t = 0

The covariant acceleration of a radial curve of the variation vanishes on its maximal interval.

theorem TauCeti.Manifold.eventually_acceleration_radialVariation_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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : ∀ᶠ (u : ℝ) in nhds 0, (CovariantDerivative.leviCivitaConnection I M).acceleration (F u) t = 0

At a parameter of the central geodesic, the radial curves of the variation near the central one have vanishing covariant acceleration.

theorem TauCeti.Manifold.variationField_radialVariation {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 w : TangentSpace I p} {F : ℝ → ℝ → M} (hF : ∀ (u t : ℝ), F u t = riemannianExp I M p (t • (v + u • w))) {t : ℝ} (ht : t ∈ geodesicInterval I M p v) : variationField I F t = (mfderiv% (riemannianExp I M p) (t • v)) (t • w)

The variation field of the radial variation at a parameter t of the central geodesic is the differential d(exp_p)_{t v}(t w) of the exponential map.

Regularity of the differential along a fixed direction

theorem TauCeti.Manifold.continuousAt_norm_angular_riemannianExp_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 w : TangentSpace I p) : ContinuousAt (fun (r : ℝ) => ‖(mfderiv% (riemannianExp I M p) (r • v)) w‖) 0

The Riemannian norm of the differential of the exponential map, applied to a fixed tangent vector w and evaluated along the line r ↦ r • v, is continuous at the centre. The norm is the varying Riemannian tangent norm, rather than a fixed model-space norm.

theorem TauCeti.Manifold.contDiffOn_inner_angular_riemannianExp {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) (w : TangentSpace I p) : ContDiffOn ℝ (↑⊤) (fun (z : TangentSpace I p) => inner ℝ ((mfderiv% (riemannianExp I M p) z) w) ((mfderiv% (riemannianExp I M p) z) w)) (expDomain I M p)

The squared Riemannian length of the differential of the exponential map, applied to a fixed tangent vector w, is smooth on the exponential domain.

Completeness at a point

def TauCeti.Manifold.IsGeodesicallyCompleteAt {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) : Prop

A Riemannian manifold is geodesically complete at p when every maximal geodesic leaving p is defined for all time.

theorem TauCeti.Manifold.expDomain_eq_univ_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} : expDomain I M p = Set.univ ↔ IsGeodesicallyCompleteAt I M p

Completeness at a point via the exponential map. The exponential map at p is defined on all of T_p M exactly when every geodesic leaving p is defined for all time.

theorem TauCeti.Manifold.isGeodesicallyCompleteAt_iff_forall_one_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] {p : M} : IsGeodesicallyCompleteAt I M p ↔ ∀ (v : TangentSpace I p), 1 ∈ geodesicInterval I M p v

Geodesic completeness at a point is equivalent to every initial velocity admitting a geodesic at time 1.

theorem TauCeti.Manifold.not_isGeodesicallyCompleteAt_iff_exists_one_notMem_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} : ¬IsGeodesicallyCompleteAt I M p ↔ ∃ (v : TangentSpace I p), 1 ∉ geodesicInterval I M p v

Failure of geodesic completeness supplies an initial velocity whose geodesic is undefined at time 1.