Hadamard space (source code)

= Hadamard space
{c}

A Hadamard space is a <complete> <CAT(0) space>. Equivalently, it is a <complete metric space> in which every pair $x,y$ has a <midpoint> $m$ satisfying
$$
d(z,m)^2\leq\frac12d(z,x)^2+\frac12d(z,y)^2-\frac14d(x,y)^2
$$
for every $z$. A <midpoint> means $d(x,m)=d(m,y)=d(x,y)/2$. Substituting a second midpoint for $z$ forces their distance to be zero, so the <midpoint> is unique.

Iterating <midpoints> defines the joining <geodesic> first at dyadic parameters. <Completeness> then supplies its points at every real parameter. The midpoint inequality extends by this approximation to the <Hadamard squared-distance inequality>, and hence to Euclidean triangle comparison. In particular, closed balls have <geodesic convexity>.

The completeness condition belongs in both formulations. The <rational numbers> with the usual distance have all rational <midpoints> and satisfy the displayed inequality, but are incomplete. A full real-parameter <geodesic> from zero to one would require irrational points. Thus the midpoint inequality alone does not make that space a Hadamard space.