Finiteness of the Riemannian distance, and the induced metric space

Manifold.riemannianEDist I x y is the infimum of the lengths of C¹ paths from x to y, an extended distance: it is ∞ as soon as no such path exists. This file identifies exactly when it is finite, and uses that to promote the extended metric space structure EMetricSpace.ofRiemannianMetric of a preconnected Riemannian manifold to an ordinary metric space structure, which is what statements about dist, ProperSpace and CompleteSpace need.

The key point is that {y | riemannianEDist I x y < ∞} is clopen: it is open because nearby points are at small Riemannian distance (eventually_riemannianEDist_lt), and its complement is open for the same reason. Hence it contains the connected component of x. Conversely a C¹ path is in particular continuous, so a point at finite Riemannian distance from x lies in the connected component of x. Together these give riemannianEDist_lt_top_iff_mem_connectedComponent, of which finiteness on a preconnected manifold is the special case that matters downstream.

Main results

• TauCeti.Manifold.riemannianEDist_lt_top_iff_mem_connectedComponent: the Riemannian distance from x to y is finite if and only if y lies in the connected component of x.
• TauCeti.Manifold.riemannianEDist_ne_top: on a preconnected manifold the Riemannian distance is never ∞.
• TauCeti.PseudoMetricSpace.ofRiemannianMetric and TauCeti.MetricSpace.ofRiemannianMetric: the (pseudo)metric space structures of a preconnected Riemannian manifold, refining PseudoEMetricSpace.ofRiemannianMetric and EMetricSpace.ofRiemannianMetric; both satisfy IsRiemannianManifold I M.
• TauCeti.IsRiemannianManifold.edist_le_pathELength and TauCeti.IsRiemannianManifold.dist_le_toReal_pathELength: the ambient (extended) distance of a Riemannian manifold, read through IsRiemannianManifold.out, is bounded by the length of any C¹ path.
• TauCeti.IsRiemannianManifold.edist_le_of_norm_mfderiv_le: the mean-value inequality for a C¹ map from a normed space into a Riemannian manifold along a segment.
• TauCeti.Manifold.le_riemannianEDist_of_forall_le_pathELength: the extended distance is bounded below by any bound valid for the lengths of all C¹ curves joining two points, since it is the infimum of those lengths.

References

• Geodesics, the exponential map, and the Hopf–Rinow theorem roadmap, Layer 0, "Distance compatibility and finiteness".
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7 §2, Def. 2.4.
• Mathlib/Geometry/Manifold/Riemannian/Basic.lean (S. Gouëzel): PseudoEMetricSpace.ofRiemannianMetric, EMetricSpace.ofRiemannianMetric, and their IsRiemannianManifold instances, which the (pseudo)metric constructions here adapt.

theorem TauCeti.Manifold.joined_of_riemannianEDist_lt_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {x y : M} (h : Manifold.riemannianEDist I x y < ⊤) : Joined x y

Two points at finite Riemannian distance are joined by a path: a C¹ path witnessing any strict upper bound on the distance is in particular continuous.

theorem TauCeti.Manifold.le_riemannianEDist_of_forall_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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {x y : M} {c : ENNReal} (h : ∀ (γ : ℝ → M), γ 0 = x → γ 1 = y → ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1) → c ≤ Manifold.pathELength I γ 0 1) : c ≤ Manifold.riemannianEDist I x y

The Riemannian extended distance is bounded below by any bound that is valid for the lengths of all C¹ curves joining the two points: it is the infimum of those lengths.

theorem TauCeti.Manifold.isOpen_setOfPred_riemannianEDist_lt_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : IsOpen {y : M | Manifold.riemannianEDist I x y < ⊤}

The set of points at finite Riemannian distance from x is open: any point close enough to a point y of this set is at Riemannian distance < 1 from y, hence at finite distance from x by the triangle inequality.

theorem TauCeti.Manifold.isClosed_setOfPred_riemannianEDist_lt_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : IsClosed {y : M | Manifold.riemannianEDist I x y < ⊤}

The set of points at finite Riemannian distance from x is closed: if y is at infinite Riemannian distance from x, then so is any point close enough to y, again by the triangle inequality.

theorem TauCeti.Manifold.isClopen_setOfPred_riemannianEDist_lt_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : IsClopen {y : M | Manifold.riemannianEDist I x y < ⊤}

The set of points at finite Riemannian distance from x is clopen.

theorem TauCeti.Manifold.riemannianEDist_lt_top_of_isPreconnected {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {s : Set M} (hs : IsPreconnected s) {x y : M} (hx : x ∈ s) (hy : y ∈ s) : Manifold.riemannianEDist I x y < ⊤

Two points of a preconnected set are at finite Riemannian distance.

theorem TauCeti.Manifold.riemannianEDist_lt_top_iff_mem_connectedComponent {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {x y : M} : Manifold.riemannianEDist I x y < ⊤ ↔ y ∈ connectedComponent x

The Riemannian distance from x to y is finite exactly when y lies in the connected component of x.

theorem TauCeti.Manifold.riemannianEDist_lt_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [PreconnectedSpace M] (x y : M) : Manifold.riemannianEDist I x y < ⊤

On a preconnected manifold, the Riemannian distance between any two points is finite.

@[simp]

theorem TauCeti.Manifold.riemannianEDist_ne_top {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [PreconnectedSpace M] (x y : M) : Manifold.riemannianEDist I x y ≠ ⊤

On a preconnected manifold, the Riemannian distance between any two points is finite. This is the hypothesis needed to turn EMetricSpace.ofRiemannianMetric into a genuine metric space.

theorem TauCeti.IsRiemannianManifold.edist_le_pathELength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {γ : ℝ → M} {a b : ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hab : a ≤ b) : edist (γ a) (γ b) ≤ Manifold.pathELength I γ a b

In a Riemannian manifold, the ambient extended distance between the endpoints of a C¹ path is at most the length of that path. This is Manifold.riemannianEDist_le_pathELength read through IsRiemannianManifold.out.

theorem TauCeti.IsRiemannianManifold.edist_le_of_norm_mfderiv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : F → M} {a b : F} {C : ℝ} (hf : ∀ z ∈ segment ℝ a b, ContMDiffAt (modelWithCornersSelf ℝ F) I 1 f z) (hC : ∀ z ∈ segment ℝ a b, ‖(mfderiv% f z) (b - a)‖ ≤ C) : edist (f a) (f b) ≤ ENNReal.ofReal C

The mean-value inequality for maps into a Riemannian manifold. Let f be a map from a real normed space to a Riemannian manifold which is C¹ at every point of the segment from a to b. If its differential along that segment sends b - a to vectors of norm at most C, then f a and f b are at extended distance at most C.

theorem TauCeti.IsRiemannianManifold.dist_eq_toReal_riemannianEDist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [PseudoMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] (x y : M) : dist x y = (Manifold.riemannianEDist I x y).toReal

In a Riemannian manifold whose ambient distance is an ordinary one, that distance is the real part of the Riemannian extended distance.

theorem TauCeti.IsRiemannianManifold.dist_le_toReal_pathELength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [PseudoMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {γ : ℝ → M} {a b : ℝ} {x y : M} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (ha : γ a = x) (hb : γ b = y) (hab : a ≤ b) (h : Manifold.pathELength I γ a b ≠ ⊤) : dist x y ≤ (Manifold.pathELength I γ a b).toReal

In a Riemannian manifold whose ambient distance is an ordinary one, the distance is bounded above by the length of any C¹ path of finite length between the two points.

theorem TauCeti.IsRiemannianManifold.exists_pathELength_lt_of_dist_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [PseudoMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsRiemannianManifold I M] {x y : M} {r : ℝ} (hr : dist x y < r) : ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1) ∧ Manifold.pathELength I γ 0 1 < ENNReal.ofReal r

In a Riemannian manifold whose ambient distance is an ordinary one, any bound r on the distance from x to y is witnessed by a C¹ path on [0, 1] of length < ENNReal.ofReal r.

@[reducible]

noncomputable def TauCeti.PseudoMetricSpace.ofRiemannianMetric {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] [PreconnectedSpace M] : PseudoMetricSpace M

The pseudometric space structure associated to a Riemannian metric on a preconnected manifold, obtained from PseudoEMetricSpace.ofRiemannianMetric now that the extended distance is known to be finite. As for the extended version, the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory, one should rather assume that there is an already existing pseudometric space structure, satisfying additionally the predicate IsRiemannianManifold I M.

Equations

• TauCeti.PseudoMetricSpace.ofRiemannianMetric I M = PseudoEMetricSpace.toPseudoMetricSpace ⋯

instance TauCeti.instIsRiemannianManifold_tauCeti {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] [PreconnectedSpace M] : IsRiemannianManifold I M

The distance of PseudoMetricSpace.ofRiemannianMetric is the infimum of the lengths of C¹ paths, i.e. the resulting pseudometric space satisfies the IsRiemannianManifold I M predicate.

@[reducible]

noncomputable def TauCeti.MetricSpace.ofRiemannianMetric {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] [PreconnectedSpace M] : MetricSpace M

The metric space structure associated to a Riemannian metric on a preconnected manifold, obtained from EMetricSpace.ofRiemannianMetric now that the extended distance is known to be finite. As for the extended version, the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory, one should rather assume that there is an already existing metric space structure, satisfying additionally the predicate IsRiemannianManifold I M.

Equations

• TauCeti.MetricSpace.ofRiemannianMetric I M = EMetricSpace.toMetricSpace ⋯

instance TauCeti.instIsRiemannianManifold_tauCeti_1 {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] [PreconnectedSpace M] : IsRiemannianManifold I M

The distance of MetricSpace.ofRiemannianMetric is the infimum of the lengths of C¹ paths, i.e. the resulting metric space satisfies the IsRiemannianManifold I M predicate.