def NegativeCurvatureInequality (M : Type u_2) [MetricSpace M] : Prop

CAT(0)/negative curvature inequality on a metric space $M$: for every pair $x, y \in M$ there exists a midpoint $m$ such that for all $z$, $d(z, m)^2 \leq \tfrac{1}{2} d(z, x)^2 + \tfrac{1}{2} d(z, y)^2 - \tfrac{1}{4} d(x, y)^2$.

noncomputable def radiusFrom {M : Type u_1} [MetricSpace M] (x : M) (Y : Set M) : ℝ

Radius of the set $Y$ as seen from the point $x$: $\sup_{y \in Y} d(x, y)$.

noncomputable def circumradius {M : Type u_1} [MetricSpace M] (Y : Set M) : ℝ

Circumradius of $Y$: $\inf_{x \in M} \sup_{y \in Y} d(x, y)$.

def IsCircumcenter {M : Type u_1} [MetricSpace M] (x : M) (Y : Set M) : Prop

$x$ is a circumcenter of $Y$ iff its enclosing radius equals the circumradius of $Y$.

structure IsometricAction (G : Type u_2) [Group G] (M : Type u_3) [MetricSpace M] : Type (max u_2 u_3)

An isometric action of a group $G$ on a metric space $M$: a scalar multiplication respecting the group identity, composition, and acting by isometries on $M$.

• smul : G → M → M
• smul_one (x : M) : self.smul 1 x = x
• smul_mul (g h : G) (x : M) : self.smul (g * h) x = self.smul g (self.smul h x)
• isometry_smul (g : G) : Isometry (self.smul g)

def IsometricAction.IsStable {M : Type u_1} [MetricSpace M] {G : Type u_2} [Group G] (act : IsometricAction G M) (Y : Set M) : Prop

A subset $Y \subseteq M$ is stable under the isometric action iff $g \cdot Y \subseteq Y$ for every $g \in G$.

def IsometricAction.IsFixedPoint {M : Type u_1} [MetricSpace M] {G : Type u_2} [Group G] (act : IsometricAction G M) (x : M) : Prop

$x$ is a fixed point of the isometric action iff $g \cdot x = x$ for all $g \in G$.

theorem radiusFrom_nonneg {M : Type u_1} [MetricSpace M] (x : M) (Y : Set M) : 0 ≤ radiusFrom x Y

The radius from a point is nonnegative.

theorem bddAbove_dist_range {M : Type u_1} [MetricSpace M] (x : M) (Y : Set M) (hbd : Bornology.IsBounded Y) : BddAbove (Set.range fun (y : ↑Y) => dist x ↑y)

For bounded $Y$, the set of distances from $x$ to elements of $Y$ is bounded above.

theorem dist_le_radiusFrom {M : Type u_1} [MetricSpace M] (x : M) {Y : Set M} (hbd : Bornology.IsBounded Y) {y : M} (hy : y ∈ Y) : dist x y ≤ radiusFrom x Y

Any point of a bounded set $Y$ lies within radiusFrom x Y from $x$.

theorem circumradius_nonneg {M : Type u_1} [MetricSpace M] (Y : Set M) : 0 ≤ circumradius Y

The circumradius is nonnegative.

theorem circumradius_le_radiusFrom {M : Type u_1} [MetricSpace M] (x : M) (Y : Set M) : circumradius Y ≤ radiusFrom x Y

The circumradius is a lower bound for radiusFrom x Y at every $x$.

theorem isometry_radiusFrom_eq {M : Type u_1} [MetricSpace M] (φ : M → M) (hφ : Isometry φ) (x : M) (Y : Set M) : radiusFrom (φ x) (φ '' Y) = radiusFrom x Y

Isometries preserve radiusFrom: if $\varphi$ is an isometry then radiusFrom (φ x) (φ '' Y) = radiusFrom x Y.

theorem circumcenter_exists (M : Type u_2) [MetricSpace M] [CompleteSpace M] (hNCI : NegativeCurvatureInequality M) (Y : Set M) (hne : Y.Nonempty) (hbd : Bornology.IsBounded Y) : ∃ (c : M), IsCircumcenter c Y

Existence of circumcenters in CAT(0) spaces: in a complete metric space satisfying the negative curvature inequality, every nonempty bounded subset $Y$ has a circumcenter $c \in M$.

theorem circumcenter_unique (M : Type u_2) [MetricSpace M] (hNCI : NegativeCurvatureInequality M) (Y : Set M) (hne : Y.Nonempty) (hbd : Bornology.IsBounded Y) (c₁ c₂ : M) (h₁ : IsCircumcenter c₁ Y) (h₂ : IsCircumcenter c₂ Y) : c₁ = c₂

Uniqueness of circumcenters in CAT(0) spaces: any two circumcenters $c_1, c_2$ of a nonempty bounded set $Y$ in a CAT(0) metric space coincide.

theorem stable_image_eq {M : Type u_1} [MetricSpace M] {G : Type u_2} [Group G] (act : IsometricAction G M) (Y : Set M) (hstab : act.IsStable Y) (g : G) : act.smul g '' Y = Y

If $Y$ is stable under the action then $g \cdot Y = Y$ as a set.

theorem BruhatTitsFixedPoint (M : Type u_2) [MetricSpace M] [CompleteSpace M] (hNCI : NegativeCurvatureInequality M) (G : Type u_3) [Group G] (act : IsometricAction G M) (Y : Set M) (hne : Y.Nonempty) (hbd : Bornology.IsBounded Y) (hstab : act.IsStable Y) : ∃ (x : M), act.IsFixedPoint x

Bruhat–Tits fixed point theorem: a group $G$ acting isometrically on a complete CAT(0) metric space $M$ and stabilizing some nonempty bounded subset $Y$ admits a global fixed point $x \in M$. The fixed point is the (unique) circumcenter of $Y$.