Completeness of the upper-half-space metric #
The upper-half-space model carries a transitive action by Riemannian isometries. The general
homogeneous-manifold completeness theorem therefore supplies the metric completeness required by
the complete field of TauCeti.HyperbolicMetric. This file records that consequence for every
finite-dimensional real inner-product space, leaving the constant-curvature calculation to the
model-specific hyperbolic development.
Main result #
TauCeti.UpperHalfSpace.completeSpace_of_riemannianMetric: the Riemannian distance of the upper-half-space metric is complete.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 3.
- W. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Proposition 3.4.15.
theorem
TauCeti.UpperHalfSpace.completeSpace_of_riemannianMetric
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
:
The Riemannian distance of the upper-half-space metric is complete in finite dimension.
The explicit uniform-space argument in the conclusion matches the metric used by
TauCeti.HyperbolicMetric.complete.