Polar length comparison in a normal domain

The Gauss lemma controls the radial part of the differential of the Riemannian exponential map. Its Cauchy--Schwarz consequence says that the radial derivative of a polar lift is no larger than the speed of its image under the exponential map. Integrating this estimate shows that a curve inside a normal neighbourhood has length at least the absolute change in the norm of its logarithm.

The comparison needs no nonvanishing hypothesis, so it also covers curves passing through the centre of the normal neighbourhood. Corner smoothing extends it from C¹ curves to piecewise C¹ curves, between any two ordered parameters of such a curve.

Main results

• TauCeti.Manifold.abs_inner_le_norm_mul_norm_mfderiv_riemannianExp: the pointwise radial differential estimate.
• IsNormalDomain.ofReal_abs_norm_riemannianLog_sub_norm_riemannianLog_le_pathELength: the polar length comparison for a C¹ curve in a normal neighbourhood.
• IsNormalDomain.ofReal_abs_norm_riemannianLog_sub_norm_riemannianLog_le_pathELength_of_piecewise: the same comparison for a piecewise C¹ curve, between any two ordered parameters.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3, Proposition 3.6.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Ch. 6.
• The smoothed-radius argument follows DoCarmoLib/Riemannian/Exponential/Minimizing.lean in the Apache-2.0 frenzymath/Poincare-Conjecture repository, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, adapted to Tau Ceti's intrinsic exponential map and normal-domain API.

theorem TauCeti.Manifold.abs_inner_le_norm_mul_norm_mfderiv_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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {v w : TangentSpace I p} (hv : v ∈ expDomain I M p) : |inner ℝ v w| ≤ ‖v‖ * ‖(mfderiv% (riemannianExp I M p) v) w‖

The pointwise polar inequality. The radial component of a tangent vector at v is no larger than the norm of its image under the differential of the Riemannian exponential map.

theorem TauCeti.Manifold.abs_inner_div_sqrt_inner_add_le_norm_mfderiv_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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {v w : TangentSpace I p} {δ : ℝ} (hδ : 0 ≤ δ) (hv : v ∈ expDomain I M p) : |inner ℝ v w| / √(inner ℝ v v + δ) ≤ ‖(mfderiv% (riemannianExp I M p) v) w‖

The pointwise polar inequality divided by the smoothed radius √(⟪v, v⟫ + δ), for δ ≥ 0.

theorem TauCeti.Manifold.ofReal_abs_norm_sub_norm_le_pathELength_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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {w : ℝ → TangentSpace I p} {a b : ℝ} (hab : a ≤ b) (hw : ContDiffOn ℝ 1 w (Set.Icc a b)) (hdom : Set.MapsTo w (Set.Icc a b) (expDomain I M p)) : ENNReal.ofReal |‖w b‖ - ‖w a‖| ≤ Manifold.pathELength I (riemannianExp I M p ∘ w) a b

Polar length comparison for the exponential map. If a C¹ path w in the tangent space stays in the natural domain of exp_p, then the length of exp_p ∘ w is at least the absolute change in the radial norm of w.

No nonvanishing hypothesis is imposed on w, so the bound also applies to paths through the origin.

theorem TauCeti.Manifold.IsNormalDomain.ofReal_abs_norm_riemannianLog_sub_norm_riemannianLog_le_pathELength {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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {U : Set (TangentSpace I p)} (h : IsNormalDomain I M p U) {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) : ENNReal.ofReal |‖riemannianLog I M p U (γ b)‖ - ‖riemannianLog I M p U (γ a)‖| ≤ Manifold.pathELength I γ a b

Polar length comparison in a normal neighbourhood. Along a C¹ curve contained in the image of a normal domain, the absolute change in the norm of its Riemannian logarithm is at most the length of the curve.

theorem TauCeti.Manifold.IsNormalDomain.ofReal_norm_riemannianLog_le_pathELength {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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {U : Set (TangentSpace I p)} (h : IsNormalDomain I M p U) {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) (hγa : γ a = p) : ENNReal.ofReal ‖riemannianLog I M p U (γ b)‖ ≤ Manifold.pathELength I γ a b

A C¹ curve from the centre of a normal neighbourhood to a point q has length at least the norm of log_p q.

theorem TauCeti.Manifold.IsNormalDomain.ofReal_abs_norm_riemannianLog_sub_norm_riemannianLog_le_pathELength_of_piecewise {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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {U : Set (TangentSpace I p)} {γ : ℝ → M} {a b : ℝ} (h : IsNormalDomain I M p U) (hγ : IsPiecewiseContMDiffOn I 1 γ a b) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) {s t : ℝ} (has : a ≤ s) (hst : s ≤ t) (htb : t ≤ b) : ENNReal.ofReal |‖riemannianLog I M p U (γ t)‖ - ‖riemannianLog I M p U (γ s)‖| ≤ Manifold.pathELength I γ s t

Polar length comparison for broken curves. Along a piecewise C¹ curve contained in the image of a normal domain, the absolute change in the norm of its Riemannian logarithm between two ordered parameters is at most the length of the curve between them.

theorem TauCeti.Manifold.IsNormalDomain.ofReal_norm_riemannianLog_le_pathELength_of_piecewise {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] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] {p : M} {U : Set (TangentSpace I p)} {γ : ℝ → M} {a b : ℝ} (h : IsNormalDomain I M p U) (hγ : IsPiecewiseContMDiffOn I 1 γ a b) (hγU : Set.MapsTo γ (Set.Icc a b) (riemannianExp I M p '' U)) (hγa : γ a = p) {t : ℝ} (ht : t ∈ Set.Icc a b) : ENNReal.ofReal ‖riemannianLog I M p U (γ t)‖ ≤ Manifold.pathELength I γ a t

Along a piecewise C¹ curve starting at the centre p of a normal neighbourhood, the length travelled up to any parameter t is at least the norm of log_p (γ t).