W-hyperbolic spaces

Stream: maths

[Horatiu Cheval]

As part of a larger project, I implemented a (very basic for now) theory of so-called $W$-hyperbolic spaces, which are essentially metric spaces $(X, d)$ endowed with a mapping $W : [0, 1] \times X \times X \to X$, satisfying certain axioms. Here, $W(\alpha, x, y)$ is intended to be interpreted as an "abstract convex combination" of parameter $\alpha$ between the points $x$ and $y$. Examples are of course vector spaces, but also structures from geodesic geometry, like $CAT(0)$ spaces.

I am wondering whether such constructions would have a place in mathlib.

[Horatiu Cheval]

The relevant code I have is here https://github.com/hcheval/tikhonov-mann/blob/master/src/wspace.lean

[Scott Morrison]

Yes, W-hyperbolic spaces are definitely within mathlib's remit. :-)

[Horatiu Cheval]

Great! Do you have any suggestions on how should I contribute them ( besides, of course, making my code adhere to the style conventions)? For example, in what file/directory should this go?