def IsSimilitude {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (f : X → Y) (c : ℝ) : Prop

A map $f : X \to Y$ between pseudo-metric spaces is a similitude of ratio $c > 0$ if $d(f(x), f(y)) = c \cdot d(x, y)$ for all $x, y \in X$.

theorem IsSimilitude.image_bounded {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {c : ℝ} (hf : IsSimilitude f c) (S : Set X) (hS : Bornology.IsBounded S) : Bornology.IsBounded (f '' S)

A similitude sends bounded sets to bounded sets.

theorem IsSimilitude.diam_image {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {c : ℝ} (hf : IsSimilitude f c) (S : Set X) (hS : Bornology.IsBounded S) : Metric.diam (f '' S) = c * Metric.diam S

A similitude of ratio $c$ scales diameters by $c$: $\mathrm{diam}(f(S)) = c \cdot \mathrm{diam}(S)$.

theorem IsSimilitude.const_eq_one_of_diam_preserved {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} {c : ℝ} (hf : IsSimilitude f c) {S : Set X} (hS_bdd : Bornology.IsBounded S) (hS_diam : Metric.diam S = 1) (hfS_diam : Metric.diam (f '' S) = 1) : c = 1

If a similitude $f$ of ratio $c$ sends a set $S$ of diameter $1$ to a set of diameter $1$, then $c = 1$ (so $f$ is an isometry on the diameter).

structure AffineCoxeterComplex.CanonicalMetric {B : Type u_1} (M : CoxeterMatrix B) (X : Type u_2) [PseudoMetricSpace X] : Type u_2

A canonical metric on the realization of an affine Coxeter complex of matrix $M$: a designated family of "chambers" $\{C\} \subseteq X$, each bounded with diameter exactly $1$.

• chambers : Set (Set X)
• chamber_bounded (C : Set X) : C ∈ self.chambers → Bornology.IsBounded C
• chamber_diam_one (C : Set X) : C ∈ self.chambers → Metric.diam C = 1
• is_affine : M.IsAffine

def AffineCoxeterComplex.CanonicalMetric.IsWInvariant {B : Type u_1} {M : CoxeterMatrix B} {X : Type u_2} [PseudoMetricSpace X] (_cm : CanonicalMetric M X) (action : M.Group → X → X) : Prop

A canonical metric on $X$ is $W$-invariant under an action $W \times X \to X$ if every $w \in W$ acts as an isometry on $X$.

noncomputable def AffineCoxeterComplex.CoxeterComplexCanonicalDist {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : AffineCoxeter.AffineCoxeterComplex E) (x y : E) : ℝ

The canonical distance on the Euclidean realization $E$ of an affine Coxeter complex: $d(x, y) = \|x - y\| / \mathrm{diam}(C)$, where $C$ is any chamber. This normalizes chambers to have diameter $1$.

theorem AffineCoxeterComplex.sc_iso_is_similitude {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeter.AffineCoxeterComplex E) (A' : AffineCoxeter.AffineCoxeterComplex E') (φ : AffineCoxeter.SimplicialComplexIso A.complex A'.complex) : ∃ (g : E →ᵃ[ℝ] E'), IsSimilitude (⇑g) (A'.chamberDiameter / A.chamberDiameter)

A simplicial-complex isomorphism between two affine Coxeter complexes realized in Euclidean spaces $E, E'$ extends to an affine similitude $g : E \to E'$ of ratio $\mathrm{diam}(C') / \mathrm{diam}(C)$.

theorem AffineCoxeterComplex.sc_iso_canonical_isometry {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {E' : Type u_3} [NormedAddCommGroup E'] [InnerProductSpace ℝ E'] (A : AffineCoxeter.AffineCoxeterComplex E) (A' : AffineCoxeter.AffineCoxeterComplex E') (φ : AffineCoxeter.SimplicialComplexIso A.complex A'.complex) (hD_eq : A.chamberDiameter = A'.chamberDiameter) : ∃ (g : E →ᵃ[ℝ] E'), ∀ (x y : E), dist (g x) (g y) = dist x y

If two affine Coxeter complexes have equal chamber diameters and are simplicially isomorphic, then the induced affine similitude is an isometry.

theorem AffineCoxeterComplex.sc_iso_canonical_isometry' {B : Type u_2} {B' : Type u_3} [DecidableEq B] [DecidableEq B'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} {X : Type u_4} {X' : Type u_5} [PseudoMetricSpace X] [PseudoMetricSpace X'] (cm : CanonicalMetric M X) (cm' : CanonicalMetric M' X') (φ : X → X') {c : ℝ} (hφ : IsSimilitude φ c) (hφ_chambers : ∀ C ∈ cm.chambers, φ '' C ∈ cm'.chambers) (h_cover : ∀ (x : X), ∃ C ∈ cm.chambers, x ∈ C) (hC_nonempty : cm.chambers.Nonempty) (x y : X) : dist (φ x) (φ y) = dist x y

Abstract canonical-metric version: a similitude $\varphi : X \to X'$ sending chambers to chambers between two canonical metrics with nonempty chamber families must be an isometry, because chamber diameter $1$ forces the similitude constant to be $1$.

theorem AffineCoxeterComplex.canonical_metric_unique {X : Type u_2} {Y : Type u_3} [PseudoMetricSpace X] [PseudoMetricSpace Y] (chambersX : Set (Set X)) (chambersY : Set (Set Y)) (hX_bdd : ∀ C ∈ chambersX, Bornology.IsBounded C) (hX_diam : ∀ C ∈ chambersX, Metric.diam C = 1) (hY_diam : ∀ C ∈ chambersY, Metric.diam C = 1) (φ : X → Y) {c : ℝ} (hφ : IsSimilitude φ c) (hφ_chambers : ∀ C ∈ chambersX, φ '' C ∈ chambersY) (hne : chambersX.Nonempty) (x y : X) : dist (φ x) (φ y) = dist x y

Uniqueness of canonical (chamber-diameter-one) metrics: a similitude between two pseudo-metric spaces sending chambers of diameter $1$ to chambers of diameter $1$ is automatically an isometry.

theorem AffineCoxeterComplex.canonical_metric_unique' {B : Type u_2} {B' : Type u_3} [DecidableEq B] [DecidableEq B'] {M : CoxeterMatrix B} {M' : CoxeterMatrix B'} {X : Type u_4} {X' : Type u_5} [PseudoMetricSpace X] [PseudoMetricSpace X'] (cm : CanonicalMetric M X) (cm' : CanonicalMetric M' X') (φ : X → X') {c : ℝ} (hφ : IsSimilitude φ c) (hφ_chambers : ∀ C ∈ cm.chambers, φ '' C ∈ cm'.chambers) (hne : cm.chambers.Nonempty) (x y : X) : dist (φ x) (φ y) = dist x y

Canonical-metric formulation of canonical_metric_unique: a similitude between two CanonicalMetric structures sending chambers to chambers is an isometry.

def AffineBuilding.apartmentMetric {V : Type u_1} [DecidableEq V] (b : Building V) : Type u_1

The type of a per-apartment metric: a function assigning to each apartment $A$ a (pseudo-)distance $V \times V \to \mathbb{R}$.

structure AffineBuilding.ApartmentMetricData {V : Type u_1} [DecidableEq V] (b : Building V) : Type (max u_1 (u_2 + 1))

Per-apartment metric data for a building: an ambient space $X$ with embedding $\iota : V \to X$ and a per-apartment pseudo-distance $\mathrm{dist}_{\mathrm{fn}}$ that is symmetric, satisfies the triangle inequality, vanishes on the diagonal, is preserved by every simplicial isomorphism between apartments, and normalizes each chamber to have diameter $1$.

• X : Type u_2
• ι : V → self.X
• dist_X : self.X → self.X → ℝ
• dist_fn : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments } → V → V → ℝ
• dist_nonneg (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y : V) : 0 ≤ self.dist_fn A x y
• dist_symm (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y : V) : self.dist_fn A x y = self.dist_fn A y x
• dist_eq_zero (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x : V) : self.dist_fn A x x = 0
• dist_triangle (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y z : V) : self.dist_fn A x z ≤ self.dist_fn A x y + self.dist_fn A y z
• iso_isometry (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (φ : SimplicialMap ↑A₁ ↑A₂) : (∀ s ∈ (↑A₁).faces, Finset.image φ.toFun s ∈ (↑A₂).faces) → ∀ (x y : V), self.dist_fn A₁ x y = self.dist_fn A₂ (φ.toFun x) (φ.toFun y)
• chamber_diam_one (A : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (C : Finset V) : (↑A).IsMaximal C → (∀ x ∈ C, ∀ y ∈ C, self.dist_fn A x y ≤ 1) ∧ ∃ x ∈ C, ∃ y ∈ C, self.dist_fn A x y = 1

def AffineBuilding.ApartmentMetricData.buildingDistVert {V : Type u_1} [DecidableEq V] {b : Building V} (md : ApartmentMetricData b) (v w : V) : ℝ

The ambient-space distance between two vertices: $d_X(\iota v, \iota w)$.

noncomputable def AffineBuilding.buildingDist {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (x y : V) : ℝ

The building distance between two vertices $x, y$: if there is some apartment containing faces through both $x$ and $y$, return the apartment-distance in any such apartment; otherwise return $0$. Well-definedness is proved below by buildingDist_well_defined_general.

theorem AffineBuilding.iso_fix_from_shared_face_and_chamber {V : Type u_1} [DecidableEq V] (b : Building V) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (σ C : Finset V) (x y : V) (hσ_A₁ : σ ∈ (↑A₁).faces) (hσ_A₂ : σ ∈ (↑A₂).faces) (hx_σ : x ∈ σ) (hy_σ : y ∈ σ) (hC_max : (↑A₁).IsMaximal C) (hC_A₂ : C ∈ (↑A₂).faces) : ∃ (φ : SimplicialMap ↑A₁ ↑A₂), φ.toFun x = x ∧ φ.toFun y = y

If two apartments share a face $\sigma$ and a chamber $C$ containing $\sigma$, then there is a simplicial isomorphism $A_1 \to A_2$ fixing both vertices $x$ and $y$ of $\sigma$.

theorem AffineBuilding.buildingDist_wellDefined_from_face_and_chamber {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (σ C : Finset V) (hσ_A₁ : σ ∈ (↑A₁).faces) (hσ_A₂ : σ ∈ (↑A₂).faces) (hC_max : (↑A₁).IsMaximal C) (hC_A₂ : C ∈ (↑A₂).faces) (x y : V) (hx_σ : x ∈ σ) (hy_σ : y ∈ σ) : md.dist_fn A₁ x y = md.dist_fn A₂ x y

When $x, y$ both lie in a face $\sigma$ shared by two apartments that also share a chamber containing $\sigma$, the apartment distances agree: $\mathrm{dist}_{A_1}(x, y) = \mathrm{dist}_{A_2}(x, y)$.

theorem AffineBuilding.buildingDist_wellDefined_from_face_and_chamber_cross {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (σ C : Finset V) (hσ_A₁ : σ ∈ (↑A₁).faces) (hσ_A₂ : σ ∈ (↑A₂).faces) (hC_max : (↑A₁).IsMaximal C) (hC_A₂ : C ∈ (↑A₂).faces) (x y : V) (hx_σ : x ∈ σ) (hy_C : y ∈ C) : md.dist_fn A₁ x y = md.dist_fn A₂ x y

A "cross" version of well-definedness: $x$ lies in a shared face $\sigma$ and $y$ lies in a shared chamber $C$; the two apartments share both $\sigma$ and $C$, so an isomorphism fixes both $x$ and $y$ and the apartment distances agree.

theorem AffineBuilding.buildingDist_wellDefined {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (v w : V) (hcommon : ∃ σ ∈ (↑A₁).faces, σ ∈ (↑A₂).faces ∧ v ∈ σ ∧ w ∈ σ) : md.dist_fn A₁ v w = md.dist_fn A₂ v w

Well-definedness of the building distance when there is a common face through $v$ and $w$: any two apartments containing such a face assign the same distance to $(v, w)$. The proof uses the standard chamber-system argument: extend $\sigma$ to a chamber in each apartment and find a third apartment containing both.

theorem AffineBuilding.buildingDist_well_defined_clean {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (v w : V) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (hv₁ : {v} ∈ (↑A₁).faces) (hw₁ : {w} ∈ (↑A₁).faces) (hv₂ : {v} ∈ (↑A₂).faces) (hw₂ : {w} ∈ (↑A₂).faces) : md.dist_fn A₁ v w = md.dist_fn A₂ v w

Well-definedness without assuming a common face: if vertices $\{v\}, \{w\}$ are both vertices of two apartments $A_1, A_2$ (no shared edge required), then $\mathrm{dist}_{A_1}(v, w) = \mathrm{dist}_{A_2}(v, w)$. The proof combines $v$ and $w$ across a third apartment via the "cross" lemma in both directions.

theorem AffineBuilding.buildingDist_well_defined_general {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (A₁ A₂ : { A : SimplicialComplex V // A ∈ b.apartmentSystem.apartments }) (x y : V) (hx₁ : ∃ s ∈ (↑A₁).faces, x ∈ s) (hy₁ : ∃ s ∈ (↑A₁).faces, y ∈ s) (hx₂ : ∃ s ∈ (↑A₂).faces, x ∈ s) (hy₂ : ∃ s ∈ (↑A₂).faces, y ∈ s) : md.dist_fn A₁ x y = md.dist_fn A₂ x y

Most general well-definedness: assuming only that $x, y$ are each contained in some face of $A_1$ and some face of $A_2$ (i.e., they are vertices of both apartments), the apartment distances agree.

def AffineBuilding.IsMetricSpace {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

The building distance defines a pseudo-metric: nonnegativity, symmetry, $d(x, x) = 0$, and triangle inequality.

structure AffineBuilding.GeodesicPath {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (x y : V) : Type u_1

A geodesic path from $x$ to $y$ in the building: a finite vertex list $v_0 = x, v_1, \ldots, v_n = y$ whose consecutive-distance sum equals $\mathrm{dist}(x, y)$, certifying the path is length-minimizing.

• vertices : List V
• head_eq : self.vertices.head? = some x
• last_eq : self.vertices.getLast? = some y
• nonempty : self.vertices ≠ []
• length_eq : (List.zipWith (buildingDist b md) self.vertices self.vertices.tail).sum = buildingDist b md x y

def AffineBuilding.IsGeodesic {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) : Prop

The building is a geodesic space: every pair of vertices is connected by some geodesic path.

def AffineBuilding.IsRetractDistNonIncreasing {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (ρ : V → V) : Prop

A retraction $\rho : V \to V$ is distance-non-increasing if $d(\rho x, \rho y) \le d(x, y)$ for all vertices $x, y$.

def AffineBuilding.IsRetractIsometryOnBase {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (ρ : V → V) (base : Finset V) : Prop

A retraction $\rho : V \to V$ is an isometry on the base chamber if $d(\rho x, \rho y) = d(x, y)$ whenever at least one of $x, y$ lies in the base chamber.

theorem AffineBuilding.telescoping_triangle_ineq {α : Type u_2} (d : α → α → ℝ) (htri : ∀ (x y z : α), d x z ≤ d x y + d y z) (hzero : ∀ (x : α), d x x ≤ 0) (l : List α) (hne : l ≠ []) : d (l.head hne) (l.getLast hne) ≤ (List.zipWith d l l.tail).sum

Telescoping triangle inequality: for any list $[v_0, \ldots, v_n]$, $d(v_0, v_n) \le \sum_{i=0}^{n-1} d(v_i, v_{i+1})$, assuming $d$ satisfies the triangle inequality and $d(x, x) \le 0$.

def AffineBuilding.LineSegment {V : Type u_1} [DecidableEq V] (b : Building V) (md : ApartmentMetricData b) (x y : V) : Set V

The (combinatorial) line segment from $x$ to $y$: the set of vertices $z$ satisfying $d(x, y) = d(x, z) + d(z, y)$ (the additivity / "between" relation).