CAT(0) spaces

A geodesic space is CAT(0) when its geodesic triangles are no fatter than their Euclidean comparison triangles. This file uses the equivalent two-point form of Bruhat and Tits: a geodesic space is CAT(0) exactly when every midpoint m of two points x, y satisfies the CN inequality

d(z, m)² ≤ (d(z, x)² + d(z, y)²) / 2 - d(x, y)² / 4 for every z.

In a Euclidean space this is an equality, Apollonius's theorem, so the inequality says that distances to a midpoint are at most their Euclidean values. Completeness is not assumed; a complete CAT(0) space is a Hadamard space.

The CN inequality propagates from midpoints to the whole of a geodesic segment: the squared distance from a fixed point is strongly convex along every geodesic segment. This is the convexity that makes barycenters of probability measures unique in CAT(0) spaces.

Main definitions

• TauCeti.IsCATZeroSpace X — X is a geodesic space satisfying the CN inequality at every midpoint.

Main results

• TauCeti.IsGeodesicSegment.strongConvexOn_dist_sq — along a geodesic segment γ from x to y in a CAT(0) space, t ↦ d(z, γ t)² is 2 d(x, y)²-strongly convex on [0, 1].
• TauCeti.IsGeodesicSegment.dist_sq_le — the resulting comparison inequality d(z, γ t)² ≤ (1 - t) d(z, x)² + t d(z, y)² - t (1 - t) d(x, y)².
• TauCeti.IsCATZeroSpace.of_isometry — a geodesic space embedding isometrically in a CAT(0) space is CAT(0).
• TauCeti.IsCATZeroSpace.of_normedAddTorsor and TauCeti.instIsCATZeroSpace — real inner product spaces, and Euclidean affine spaces over them, are CAT(0).

References

• M. R. Bridson and A. Haefliger, Metric Spaces of Non-Positive Curvature, Grundlehren der mathematischen Wissenschaften 319, Springer, 1999, Chapter II.1, Exercise 1.9(1).
• F. Bruhat and J. Tits, Groupes réductifs sur un corps local, Publ. Math. IHÉS 41 (1972), 5--251, §3.2.
• K.-T. Sturm, Probability measures on metric spaces of nonpositive curvature, in Heat Kernels and Analysis on Manifolds, Graphs, and Metric Spaces, Contemp. Math. 338 (2003), 357--390.

class TauCeti.IsCATZeroSpace (X : Type u_1) [PseudoMetricSpace X] extends TauCeti.IsGeodesicSpace X : Prop

A CAT(0) space, in the Bruhat--Tits form: a geodesic space in which every midpoint m of two points x, y satisfies the CN inequality d(z, m)² ≤ (d(z, x)² + d(z, y)²) / 2 - d(x, y)² / 4 for every z. For geodesic spaces this is equivalent to the comparison-triangle definition.

• exists_isGeodesicSegment (x y : X) : ∃ (γ : ℝ → X), IsGeodesicSegment γ x y
• dist_sq_le_of_dist_eq_half {x y m : X} (hx : dist x m = dist x y / 2) (hy : dist m y = dist x y / 2) (z : X) : dist z m ^ 2 ≤ (dist z x ^ 2 + dist z y ^ 2) / 2 - dist x y ^ 2 / 4

  The CN inequality of Bruhat and Tits at a midpoint m of x and y.

theorem TauCeti.IsGeodesicSegment.strongConvexOn_dist_sq {X : Type u_1} [PseudoMetricSpace X] [IsCATZeroSpace X] {γ : ℝ → X} {x y : X} (hγ : IsGeodesicSegment γ x y) (z : X) : StrongConvexOn (Set.Icc 0 1) (2 * dist x y ^ 2) fun (t : ℝ) => dist z (γ t) ^ 2

Strong convexity of the squared distance in a CAT(0) space. Along a geodesic segment γ from x to y, the squared distance t ↦ d(z, γ t)² from any point z is 2 d(x, y)²-strongly convex on [0, 1].

theorem TauCeti.IsGeodesicSegment.dist_sq_le {X : Type u_1} [PseudoMetricSpace X] [IsCATZeroSpace X] {γ : ℝ → X} {x y : X} (hγ : IsGeodesicSegment γ x y) (z : X) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : dist z (γ t) ^ 2 ≤ (1 - t) * dist z x ^ 2 + t * dist z y ^ 2 - t * (1 - t) * dist x y ^ 2

The CAT(0) comparison inequality along a geodesic segment. If γ is a geodesic segment from x to y in a CAT(0) space, then for every z and t ∈ [0, 1], d(z, γ t)² ≤ (1 - t) d(z, x)² + t d(z, y)² - t (1 - t) d(x, y)².

theorem TauCeti.IsCATZeroSpace.of_isometry {X : Type u_1} [PseudoMetricSpace X] [IsCATZeroSpace X] {Y : Type u_2} [PseudoMetricSpace Y] [IsGeodesicSpace Y] {f : Y → X} (hf : Isometry f) : IsCATZeroSpace Y

A geodesic space that embeds isometrically in a CAT(0) space is CAT(0): the CN inequality only involves distances, and an isometry sends midpoints to midpoints. The embedding need not be onto, and its image need not be a geodesically convex subset of X; the geodesics of Y are assumed.

theorem TauCeti.IsCATZeroSpace.of_normedAddTorsor {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] : IsCATZeroSpace P

A Euclidean affine space, a metric torsor over a real inner product space, is CAT(0): the CN inequality is Apollonius's theorem. This is a theorem rather than an instance because the acting space V cannot be found from the torsor; see TauCeti.instIsCATZeroSpace for the case of an inner product space acting on itself.

instance TauCeti.instIsCATZeroSpace {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsCATZeroSpace E

A real inner product space is CAT(0).