[isabelle-dev] New AFP entry Gromov Hyperbolicity in devel

[Tobias Nipkow]

We have a new AFP entry in the development branch of the AFP:

Gromov Hyperbolicity
Sebastien Gouezel

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 quasi-isometries, we define and study the Gromov boundary 
and its associated distance, and prove that a quasi-isometry 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 Gromov-hyperbolic 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, quasi-isometries, Lipschitz maps, geodesic spaces, the Hausdorff 
distance, the Cauchy completion of a metric space, and the exponential on 
extended real numbers.

https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html

You will also need to pull from the Isabelle development repo.

Enjoy!

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180118/f4963c3f/attachment.p7s>