The complete hyperbolic metric on upper half-space #
Package the standard metric (‖dx‖² + dt²) / t² with its proved completeness and
constant-curvature tensor as a HyperbolicMetric. This gives an explicit metric witness
for hyperbolic space in every positive dimension, usable by the hyperbolic volume API.
The underlying Riemannian metric is exactly the previously installed upper-half-space metric.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 3 (hyperbolic space in the upper-half-space model).
noncomputable def
TauCeti.UpperHalfSpace.hyperbolicMetric
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
:
The standard complete metric of constant curvature -1 on upper half-space.
Instances For
@[simp]
theorem
TauCeti.UpperHalfSpace.hyperbolicMetric_toRiemannianMetric
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
:
Forgetting completeness and curvature recovers the standard upper-half-space metric.
theorem
TauCeti.UpperHalfSpace.isHyperbolic
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
:
Upper half-space with its standard manifold structure admits a complete hyperbolic metric.