The Gauss lemma for the Riemannian exponential map

The Gauss lemma says that the differential of the exponential map preserves the radial component of a tangent vector. If v belongs to the natural domain of exp_p, then

<d(exp_p)_v(v), d(exp_p)_v(w)> = <v, w>.

The proof uses the radial variation F(u,t) = exp_p(t (v + u w)). Its t-curves are geodesics, so they have constant speed. Metric compatibility and the symmetry of the two mixed covariant derivatives turn the derivative in t of <∂_u F, ∂_t F> into <v,w>. Integrating from t = 0, where the transverse field vanishes, gives the identity at t = 1.

The statement is made on the full natural domain of the exponential map. In particular, every normal domain inherits it without choosing a smaller ball.

Main result

• TauCeti.Manifold.inner_mfderiv_riemannianExp_radial: the differential of the exponential map preserves inner products with the radial direction.
• TauCeti.Manifold.norm_mfderiv_riemannianExp_radial: the differential of the exponential map preserves the norm of the radial direction.
• TauCeti.Manifold.inner_mfderiv_riemannianExp_unit_radial and TauCeti.Manifold.inner_mfderiv_riemannianExp_radial_angular: unit radial directions stay unit, and stay orthogonal to perpendicular directions, under the differential of the exponential map.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3, Lemma 3.5.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Lemma 6.3.
• The organization follows DoCarmoLib/Riemannian/Exponential/GaussLemma.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, replacing its chart-level connection and exponential-map infrastructure with Tau Ceti's intrinsic APIs.

The radial variation

The Gauss lemma is proved by differentiating the radial variation

F (u, t) = exp_p (t • (v + u • w))

of the geodesic t ↦ exp_p (t • v). Each radial curve of the variation is a maximal geodesic and the variation is smooth wherever the exponential map is (TauCeti.Manifold.radialVariation_eq_maximalGeodesic, TauCeti.Manifold.contMDiffAt_radialVariation). The facts below add what the variational argument consumes beyond these: the transverse covariant derivative of the radial velocity field is determined by the constant speed of those geodesics. As in the shared API, the variation is a function F together with its defining equation.

theorem TauCeti.Manifold.inner_mfderiv_riemannianExp_radial {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} (hv : v ∈ expDomain I M p) : inner ℝ ((mfderiv% (riemannianExp I M p) v) v) ((mfderiv% (riemannianExp I M p) v) w) = inner ℝ v w

The Gauss lemma. The differential of the Riemannian exponential map preserves the inner product with the radial direction at every vector in its natural domain.

@[simp]

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

Radial norm preservation. The differential of the Riemannian exponential map preserves the norm of the radial direction at every vector in its natural domain.

theorem TauCeti.Manifold.inner_mfderiv_riemannianExp_unit_radial {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} {r : ℝ} (hmem : r • v ∈ expDomain I M p) (hv : ‖v‖ = 1) : inner ℝ ((mfderiv% (riemannianExp I M p) (r • v)) v) ((mfderiv% (riemannianExp I M p) (r • v)) v) = 1

The differential of the exponential map at r • v sends a unit radial direction v to a unit vector.

theorem TauCeti.Manifold.inner_mfderiv_riemannianExp_radial_angular {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} {r : ℝ} (hmem : r • v ∈ expDomain I M p) (hvw : inner ℝ v w = 0) : inner ℝ ((mfderiv% (riemannianExp I M p) (r • v)) v) ((mfderiv% (riemannianExp I M p) (r • v)) (r • w)) = 0

Gauss orthogonality in radial and angular coordinates. The differential of the exponential map at r • v sends a radial direction v and a vector r • w with w ⟂ v to orthogonal vectors.