
Gromov
Hyperbolicity
Title: 
Gromov Hyperbolicity 
Author:

Sebastien Gouezel

Submission date: 
20180116 
Abstract: 
A geodesic metric space is Gromov hyperbolic if all its geodesic
triangles are thin, i.e., every side is contained in a fixed
thickening of the two other sides. While this definition looks
innocuous, it has proved extremely important and versatile in modern
geometry since its introduction by Gromov. We formalize the basic
classical properties of Gromov hyperbolic spaces, notably the Morse
lemma asserting that quasigeodesics are close to geodesics, the
invariance of hyperbolicity under quasiisometries, we define and
study the Gromov boundary and its associated distance, and prove that
a quasiisometry between Gromov hyperbolic spaces extends to a
homeomorphism of the boundaries. We also prove a less classical
theorem, by Bonk and Schramm, asserting that a Gromov hyperbolic space
embeds isometrically in a geodesic Gromovhyperbolic space. As the
original proof uses a transfinite sequence of Cauchy completions, this
is an interesting formalization exercise. Along the way, we introduce
basic material on isometries, quasiisometries, Lipschitz maps,
geodesic spaces, the Hausdorff distance, the Cauchy completion of a
metric space, and the exponential on extended real numbers. 
BibTeX: 
@article{Gromov_HyperbolicityAFP,
author = {Sebastien Gouezel},
title = {Gromov Hyperbolicity},
journal = {Archive of Formal Proofs},
month = jan,
year = 2018,
note = {\url{http://isaafp.org/entries/Gromov_Hyperbolicity.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Ergodic_Theory 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

