The Riemannian distance on inner product spaces and their convex open subsets

The standard Riemannian metric of an inner product space F restricts to any open subset U ⊆ F through the open-submanifold instances of TauCeti.Geometry.Manifold.Riemannian.Restriction. This file computes the resulting Riemannian distance when U is convex: straight segments stay in U, so every two points of U are joined by a curve of length exactly the ambient norm distance, while no curve can be shorter than that chord. Hence

• the Riemannian extended distance of a convex open subset equals the ambient norm distance;
• with its ambient metric, a convex open subset satisfies IsRiemannianManifold, which makes the ordinary-metric layer (dist, closed balls, ProperSpace, CompleteSpace) available on it.

This computation lets examples such as the open unit ball use the ordinary metric presentation. No finite-dimensionality assumption is needed: convexity is the only substantive hypothesis. The general facts about path length used along the way live in their canonical modules: TauCeti.Manifold.pathELength_lineMap (Riemannian.PathELength), and TauCeti.Manifold.pathELength_subtypeVal_comp (Riemannian.Restriction). That module also proves TopologicalSpace.Opens.riemannianEDist_le_riemannianEDist_subtype: restriction to any open submanifold cannot decrease distance.

Main results

• TopologicalSpace.Opens.riemannianEDist_eq_enorm_sub_of_convex: on a convex open subset, the restricted Riemannian extended distance is the ambient norm distance.
• TopologicalSpace.Opens.isRiemannianManifold_of_convex: the ambient metric makes a convex open subset a Riemannian manifold.
• TopologicalSpace.Opens.exists_pathELength_eq_edist_of_convex: any two points of a convex open subset are joined by a C¹ path whose Riemannian length is their distance.

References

• The ambient distance computation adapts the proof of the IsRiemannianManifold 𝓘(ℝ, F) F instance in Mathlib, Mathlib/Geometry/Manifold/Riemannian/Basic.lean by S. Gouëzel.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 1, §2 (arc length; the length of a segment).

Convex open subsets of an inner product space

theorem TopologicalSpace.Opens.pathELength_convexSegment {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (U : Opens F) (hU : Convex ℝ ↑U) (x y : ↥U) : Manifold.pathELength (modelWithCornersSelf ℝ F) ((↑U).convexSegment hU x y) 0 1 = ‖↑x - ↑y‖ₑ

The length of a straight segment in a convex open subset is the ambient norm distance between its endpoints.

@[simp]

theorem TopologicalSpace.Opens.riemannianEDist_eq_enorm_sub_of_convex {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (U : Opens F) (hU : Convex ℝ ↑U) (x y : ↥U) : Manifold.riemannianEDist (modelWithCornersSelf ℝ F) x y = ‖↑x - ↑y‖ₑ

The Riemannian distance of a convex open subset is the ambient norm distance. For an open subset U of a real inner product space F, endowed with the restriction of the standard Riemannian metric, the Riemannian extended distance between two points of U equals their norm distance read in F: the straight segment stays in U and realizes the distance. Together with TopologicalSpace.Opens.isRiemannianManifold_of_convex, this identifies the ambient metric with the distance induced by the restricted Riemannian metric.

theorem TopologicalSpace.Opens.isRiemannianManifold_of_convex {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (U : Opens F) (hU : Convex ℝ ↑U) : IsRiemannianManifold (modelWithCornersSelf ℝ F) ↥U

A convex open subset of an inner product space, endowed with its ambient metric, satisfies the IsRiemannianManifold predicate: its ambient extended distance is the infimum of the lengths of C¹ curves, because that infimum is exactly the norm distance.

Distance-realizing segments in convex open subsets

theorem TopologicalSpace.Opens.pathELength_convexSegment_eq_edist {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (U : Opens F) (hU : Convex ℝ ↑U) (x y : ↥U) : Manifold.pathELength (modelWithCornersSelf ℝ F) ((↑U).convexSegment hU x y) 0 1 = edist x y

A straight segment in a convex open subset realizes the ambient distance between its endpoints.

theorem TopologicalSpace.Opens.exists_pathELength_eq_edist_of_convex {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (U : Opens F) (hU : Convex ℝ ↑U) (x y : ↥U) : ∃ (γ : ℝ → ↥U), ContMDiffOn (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ F) 1 γ (Set.Icc 0 1) ∧ γ 0 = x ∧ γ 1 = y ∧ Manifold.pathELength (modelWithCornersSelf ℝ F) γ 0 1 = edist x y

Any two points of a convex open subset of a real inner-product space are joined by a C¹ path whose Riemannian length is their ambient distance.