(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹The Bonk Schramm extension› theory Bonk_Schramm_Extension imports Morse_Gromov_Theorem begin text ‹We want to show that any metric space is isometrically embedded in a metric space which is geodesic (i.e., there is an embedded geodesic between any two points) and complete. There are many such constructions, but a very interesting one has been given by Bonk and Schramm in~\<^cite>‹"bonk_schramm"›, together with an additional property of the completion: if the space is delta-hyperbolic (in the sense of Gromov), then its completion also is, with the same constant delta. It follows in particular that a $0$-hyperbolic space embeds in a $0$-hyperbolic geodesic space, i.e., a metric tree (there is an easier direct construction in this case). Another embedding of a metric space in a geodesic one is constructed by Mineyev~\<^cite>‹"mineyev"›, it is more canonical in a sense (isometries of the original space extend to the new space), but it is not clear if it preserves hyperbolicity. The argument of Bonk and Schramm goes as follows: - first, if one wants to add the middle of a pair of points $a$ and $b$ in a space $E$, there is a nice formula for the distance on a new space $E \cup \{*\}$ (where $*$ will by construction be a middle of $a$ and $b$). - by transfinite induction on all the pair of points in the space, one adds all the missing middles - then one completes the space - then one adds all the middles - then one goes on like that, transfinitely many times - at some point, the process stops for cardinality reasons The resulting space is complete and has middles for all pairs of points. It is then standard that it is geodesic (this is proved in \verb+Geodesic_Spaces.thy+). Implementing this construction in Isabelle is interesting and nontrivial, as transfinite induction is not that easy, especially when intermingled with metric completion (i.e., taking the quotient space of all Cauchy sequences). In particular, taking sequences of metric completions would mean changing types at each step, along a transfinite number of steps. It does not seem possible to do it naively in this way. We avoid taking quotients in the middle of the argument, as this is too messy. Instead, we define a pseudo-distance (i.e., a function satisyfing the triangular inequality, but such that $d(x,y)$ can vanish even if $x$ and $y$ are different) on an increasing set, which should contain middles and limits of Cauchy sequences (identified with their defining Cauchy sequence). Thus, we consider a datatype containing points in the original space and closed under two operations: taking a pair of points in the datatype (we think of the resulting pair as the middle of the pair) and taking a sequence with values in the datatype (we think of the resulting sequence as the limit of the sequence if it is Cauchy, for a distance yet to be defined, and as something we discard if the sequence is not Cauchy). Defining such an object is apparently not trivial. However, it is well defined, for cardinality reasons, as this process will end after the continuum cardinality iterations (as a sequence taking value in the continuum cardinality is in fact contained in a strictly smaller ordinal, which means that all sequences in the construction will appear at a step strictly before the continuum cardinality). The datatype construction in Isabelle/HOL contains these cardinality considerations as an automatic process, and is thus able to construct the datatype directly, without the need for any additional proof! Then, we define a wellorder on the datatype, such that every middle and every sequence appear after each of its ancestors. This construction of a wellorder should work for any datatype, but we provide a naive proof in our use case. Then, we define, inductively on $z$, a pseudodistance on the pair of points in $\{x : x \leq z\}$. In the induction, one should add one point at a time. If it is a middle, one uses the Bonk-Schramm recipe. If it is a sequence, then either the sequence is Cauchy and one uses the limit of the distances to the points in the sequence, or it is not Cauchy and one discards the new point by setting $d(a,a) = 1$. (This means that, in the Bonk-Schramm recipe, we only use the points with $d(x,x) = 0$, and show the triangular inequality there). In the end, we obtain a space with a pseudodistance. The desired space is obtained by quotienting out the space $\{x : d(x,x) = 0\}$ by the equivalence relation given by $d(x,y) = 0$. The triangular inequality for the pseudo-distance shows that it descends to a genuine distance on the quotient. This is the desired geodesic complete extension of the original space. › subsection ‹Unfolded Bonk Schramm extension› text ‹The unfolded Bonk Schramm extension, as explained at the beginning of this file, is a type made of the initial type, adding all possible middles and all possible limits of Cauchy sequences, without any quotienting process›