The Riemannian distance on a normal ball

Let U be a normal domain at p containing the closed tangent ball of radius r. For every v in that ball, the radial geodesic t ↦ exp_p (t • v) realizes the Riemannian distance from p to exp_p v:

edist p (exp_p v) = ‖v‖.

For points strictly inside a tangent ball, its open-ball containment in U suffices: choose a smaller closed ball around the origin before applying the distance identity.

Consequently the geodesic balls exp_p '' ball 0 r and exp_p '' closedBall 0 r are the metric balls of radius r about p. For a point q outside the geodesic ball, the distance is

edist p q = r + infEDist q (exp_p '' sphere 0 r).

These identities supply the local minimizing theory used to propagate distance along a geodesic when proving that an everywhere-defined exponential map yields minimizing geodesics between any two points.

Main results

In the namespace TauCeti.Manifold.IsNormalDomain:

• edist_riemannianExp_eq: exp_p preserves the distance from the centre of a normal ball, and dist_riemannianExp_eq its version for an ordinary metric. The _of_mem_ball variants use only open-ball containment.
• pathELength_riemannianExp_smul_eq_edist: the radial geodesic segment realizes the distance between its endpoints.
• edist_eq_enorm_riemannianLog: the distance from p is the norm of the logarithm.
• image_riemannianExp_ball and image_riemannianExp_closedBall: geodesic balls are metric balls.
• edist_eq_ofReal_add_infEDist: the distance to a point outside a geodesic ball is its radius plus the distance to the geodesic sphere.

In the namespace TauCeti.Manifold:

• exists_dist_riemannianExp_eq_dist_sub: a sufficiently small geodesic sphere about x has a point whose distance to any q decreases by the radius.

References

• The Apache-2.0 frenzymath/Poincare-Conjecture formalization, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, especially DoCarmoLib/Riemannian/Exponential/NormalBallEDist.lean.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3, Proposition 3.6 and its corollary, and Ch. 7, §2, the proof of Theorem 2.8.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, Proposition 6.11 and Corollary 6.13.

theorem TauCeti.Manifold.IsNormalDomain.edist_riemannianExp_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hv : v ∈ Metric.closedBall 0 r) : edist p (riemannianExp I M p v) = ‖v‖ₑ

Radial geodesics realize the distance on a normal ball. If the closed tangent ball of radius r lies in a normal domain at p, then for every v in that ball the distance from p to exp_p v is ‖v‖.

theorem TauCeti.Manifold.IsNormalDomain.edist_riemannianExp_eq_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) (hv : v ∈ Metric.ball 0 r) : edist p (riemannianExp I M p v) = ‖v‖ₑ

The radial distance identity for a vector strictly inside a tangent ball contained in a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_riemannianExp_smul_eq_edist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hv : v ∈ Metric.closedBall 0 r) : Manifold.pathELength I (fun (t : ℝ) => riemannianExp I M p (t • v)) 0 1 = edist p (riemannianExp I M p v)

A radial geodesic segment in a normal ball is minimizing: its length is the distance between its endpoints.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_riemannianExp_smul_eq_edist_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) (hv : v ∈ Metric.ball 0 r) : Manifold.pathELength I (fun (t : ℝ) => riemannianExp I M p (t • v)) 0 1 = edist p (riemannianExp I M p v)

A radial segment to a point strictly inside a normal tangent ball is minimizing.

theorem TauCeti.Manifold.IsNormalDomain.edist_eq_enorm_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {q : M} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hq : q ∈ riemannianExp I M p '' Metric.closedBall 0 r) : edist p q = ‖riemannianLog I M p U q‖ₑ

On a normal ball the distance from the centre is the norm of the Riemannian logarithm.

theorem TauCeti.Manifold.IsNormalDomain.edist_eq_enorm_riemannianLog_of_mem_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {q : M} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) (hq : q ∈ riemannianExp I M p '' Metric.ball 0 r) : edist p q = ‖riemannianLog I M p U q‖ₑ

On an open normal ball, the distance from the centre is the norm of the logarithm.

theorem TauCeti.Manifold.IsNormalDomain.edist_eq_ofReal_add_infEDist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {q : M} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hr : 0 ≤ r) (hq : q ∉ riemannianExp I M p '' Metric.ball 0 r) : edist p q = ENNReal.ofReal r + Metric.infEDist q (riemannianExp I M p '' Metric.sphere 0 r)

The distance to a point outside a geodesic ball. If the closed tangent ball of radius r ≥ 0 lies in a normal domain at p and q lies outside the geodesic ball exp_p '' ball 0 r, then the distance from p to q is r plus the distance from q to the geodesic sphere exp_p '' sphere 0 r.

theorem TauCeti.Manifold.IsNormalDomain.image_riemannianExp_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hr : 0 ≤ r) : riemannianExp I M p '' Metric.closedBall 0 r = Metric.closedEBall p (ENNReal.ofReal r)

Closed geodesic balls are closed metric balls. If the closed tangent ball of radius r ≥ 0 lies in a normal domain at p, then exp_p maps it onto the closed metric ball of radius r about p.

theorem TauCeti.Manifold.IsNormalDomain.image_riemannianExp_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [EMetricSpace 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] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} [IsRiemannianManifold I M] (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) : riemannianExp I M p '' Metric.ball 0 r = Metric.eball p (ENNReal.ofReal r)

Geodesic balls are metric balls. If the open tangent ball of radius r lies in a normal domain at p, then its exponential image is the open metric ball of radius r about p.

theorem TauCeti.Manifold.IsNormalDomain.dist_riemannianExp_eq {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] [IsRiemannianManifold I M] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hU : Metric.closedBall 0 r ⊆ U) (hv : v ∈ Metric.closedBall 0 r) : dist p (riemannianExp I M p v) = ‖v‖

If the closed tangent ball of radius r lies in a normal domain at p, then the distance from p to exp_p v is ‖v‖ for every v in that ball; see edist_riemannianExp_eq.

theorem TauCeti.Manifold.IsNormalDomain.dist_riemannianExp_eq_of_mem_ball {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] [IsRiemannianManifold I M] {p : M} {U : Set (TangentSpace I p)} {r : ℝ} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) (hv : v ∈ Metric.ball 0 r) : dist p (riemannianExp I M p v) = ‖v‖

The ordinary distance identity for a vector strictly inside a tangent ball contained in a normal domain.

theorem TauCeti.Manifold.exists_dist_riemannianExp_eq_dist_sub {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] [IsRiemannianManifold I M] (x q : M) : ∃ ε > 0, ∀ (δ : ℝ), 0 ≤ δ → δ < ε → δ ≤ dist x q → ∃ w ∈ expDomain I M x, ‖w‖ = δ ∧ dist (riemannianExp I M x w) q = dist x q - δ

The nearest point of a small geodesic sphere. About every point x there is a radius ε > 0 such that, for every 0 ≤ δ < ε with δ ≤ dist x q, some tangent vector w of norm δ in the domain of exp_x satisfies dist (exp_x w) q = dist x q - δ.