def AffineBuilding.BoundedAboveOn {V : Type} (f : V → ℝ) (S : Set V) : Prop

$f$ is bounded above on the set $S$: $∃ c, ∀ z ∈ S, f(z) ≤ c$.

def AffineBuilding.BoundedBelowOn {V : Type} (f : V → ℝ) (S : Set V) : Prop

$f$ is bounded below on $S$: $∃ c, ∀ z ∈ S, c ≤ f(z)$.

structure AffineBuilding.AffineFunctional {V : Type} [DecidableEq V] (b : Building V) : Type

An affine functional on an apartment $A$: a function $V → ℝ$ which is affine along the apartment's geodesic combinations.

• apartment : SimplicialComplex V
• apartment_mem : self.apartment ∈ b.apartmentSystem.apartments
• toFun : V → ℝ
• affineComb : ℝ → V → V → V
• isAffine (t : ℝ) (x y : V) : (∃ s ∈ self.apartment.faces, x ∈ s) → (∃ s ∈ self.apartment.faces, y ∈ s) → self.toFun (self.affineComb t x y) = t * self.toFun x + (1 - t) * self.toFun y

structure AffineBuilding.Wall {V : Type} [DecidableEq V] (b : Building V) : Type

A wall $\eta$ in an apartment: the zero-set of an affine functional, together with its two half-apartments $\eta^+, \eta^-$ and the axioms that the functional is unbounded in any sector direction and has a definite sign on each sector.

• apartment : SimplicialComplex V
• apartment_mem : self.apartment ∈ b.apartmentSystem.apartments
• vertices : Set V
• vertices_in_apartment (v : V) : v ∈ self.vertices → ∃ s ∈ self.apartment.faces, v ∈ s
• functional : V → ℝ
• affineComb : ℝ → V → V → V
• functionalIsAffine (t : ℝ) (x y : V) : (∃ s ∈ self.apartment.faces, x ∈ s) → (∃ s ∈ self.apartment.faces, y ∈ s) → self.functional (self.affineComb t x y) = t * self.functional x + (1 - t) * self.functional y
• functional_vanishes (v : V) : v ∈ self.vertices → self.functional v = 0
• halfPos : Set V
• halfNeg : Set V
• halfPos_def (v : V) : (∃ s ∈ self.apartment.faces, v ∈ s) → (v ∈ self.halfPos ↔ 0 ≤ self.functional v)
• halfNeg_def (v : V) : (∃ s ∈ self.apartment.faces, v ∈ s) → (v ∈ self.halfNeg ↔ self.functional v ≤ 0)
• halfPos_in_apartment (v : V) : v ∈ self.halfPos → ∃ s ∈ self.apartment.faces, v ∈ s
• halfNeg_in_apartment (v : V) : v ∈ self.halfNeg → ∃ s ∈ self.apartment.faces, v ∈ s
• functional_unbounded_on_sectors (S : Sector b) : S.apartment = self.apartment → ∀ (M : ℝ), (∃ v ∈ S.vertices, self.functional v > M) ∨ ∃ v ∈ S.vertices, self.functional v < -M
• functional_definite_sign (S : Sector b) : S.apartment = self.apartment → ∀ (f : V → ℝ), (∀ v ∈ self.vertices, f v = 0) → (∀ v ∈ S.vertices, f S.baseVertex ≤ f v) ∨ ∀ v ∈ S.vertices, f v ≤ f S.baseVertex

theorem AffineBuilding.Wall.pos_nonneg {V : Type} [DecidableEq V] {b : Building V} (eta : Wall b) (v : V) : v ∈ eta.halfPos → 0 ≤ eta.functional v

The wall functional is nonnegative on its positive half-apartment.

theorem AffineBuilding.Wall.neg_nonpos {V : Type} [DecidableEq V] {b : Building V} (eta : Wall b) (v : V) : v ∈ eta.halfNeg → eta.functional v ≤ 0

The wall functional is nonpositive on its negative half-apartment.

theorem AffineBuilding.Wall.sector_partition {V : Type} [DecidableEq V] {b : Building V} (eta : Wall b) (S : Sector b) (hS : S.apartment = eta.apartment) (v : V) : v ∈ S.vertices → v ∈ eta.halfPos ∨ v ∈ eta.halfNeg ∨ v ∈ eta.vertices

A wall partitions the vertices of a sector into $\eta^+$, $\eta^-$, and the wall itself.

theorem AffineBuilding.Wall.sector_unbounded {V : Type} [DecidableEq V] {b : Building V} (eta : Wall b) (S : Sector b) (hS : S.apartment = eta.apartment) : ¬((∃ (c : ℝ), ∀ z ∈ S.vertices, eta.functional z ≤ c) ∧ ∃ (c : ℝ), ∀ z ∈ S.vertices, c ≤ eta.functional z)

The wall functional cannot be simultaneously bounded above and below on a sector.

structure AffineBuilding.HalfApartment {V : Type} [DecidableEq V] (b : Building V) : Type

A half-apartment: a subset of an apartment equal to one of the canonical halves $\eta^+$ or $\eta^-$ of some wall $\eta$.

• apartment : SimplicialComplex V
• apartment_mem : self.apartment ∈ b.apartmentSystem.apartments
• wall : Wall b
• wall_in_apartment : self.wall.apartment = self.apartment
• vertices : Set V
• vertices_in_apartment (v : V) : v ∈ self.vertices → ∃ s ∈ self.apartment.faces, v ∈ s
• is_canonical : self.vertices = self.wall.halfPos ∨ self.vertices = self.wall.halfNeg

def AffineBuilding.AffineFunctional.VanishesOnWall {V : Type} [DecidableEq V] {b : Building V} (af : AffineFunctional b) (eta : Wall b) : Prop

An affine functional vanishes on the wall $\eta$ if it agrees on the apartment and is zero on every wall vertex.

theorem AffineBuilding.sector_affine_decomposition {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (af : AffineFunctional b) (_haf_apt : af.apartment = S.apartment) : ∃ (linear_part : V → ℝ), (∀ v ∈ S.vertices, af.toFun v = af.toFun S.baseVertex + linear_part v) ∧ linear_part S.baseVertex = 0

Decomposition: any affine functional on a sector can be written as a constant (value at the base) plus a linear part vanishing at the base.

theorem AffineBuilding.linear_part_definite_sign {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (af : AffineFunctional b) (eta : Wall b) (_haf_apt : af.apartment = S.apartment) (heta_apt : eta.apartment = S.apartment) (hvanish : af.VanishesOnWall eta) (linear_part : V → ℝ) (hdecomp : ∀ v ∈ S.vertices, af.toFun v = af.toFun S.baseVertex + linear_part v) (_hbase_zero : linear_part S.baseVertex = 0) : (∀ v ∈ S.vertices, 0 ≤ linear_part v) ∨ ∀ v ∈ S.vertices, linear_part v ≤ 0

The linear part of an affine functional vanishing on a wall has a definite sign on a sector parallel to that wall.

theorem AffineBuilding.affine_functional_bounded_on_sector {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (af : AffineFunctional b) (eta : Wall b) (haf_apt : af.apartment = S.apartment) (heta_apt : eta.apartment = S.apartment) (hvanish : af.VanishesOnWall eta) : BoundedAboveOn af.toFun S.vertices ∨ BoundedBelowOn af.toFun S.vertices

An affine functional vanishing on a wall is bounded above or below on any sector.

def AffineBuilding.signedDistToWall {V : Type} [DecidableEq V] {b : Building V} (af : AffineFunctional b) (_eta : Wall b) (z : V) : ℝ

Signed distance to the wall via the chosen affine functional.

def AffineBuilding.distToWall {V : Type} [DecidableEq V] {b : Building V} (af : AffineFunctional b) (eta : Wall b) (z : V) : ℝ

(Unsigned) distance to the wall: absolute value of signedDistToWall.

def AffineBuilding.DistBoundedInHalfApartment {V : Type} [DecidableEq V] {b : Building V} (af : AffineFunctional b) (eta : Wall b) (S : Sector b) (H : HalfApartment b) : Prop

The wall-distance is bounded above by some $M$ on the intersection of a sector with a half-apartment.

def AffineBuilding.DistUnboundedInHalfApartment {V : Type} [DecidableEq V] {b : Building V} (af : AffineFunctional b) (eta : Wall b) (S : Sector b) (H : HalfApartment b) : Prop

The negation of DistBoundedInHalfApartment: wall-distance is unbounded.

theorem AffineBuilding.wall_distance_bounded_one_side {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) : ∃ (af : AffineFunctional b) (H₁ : HalfApartment b) (H₂ : HalfApartment b), af.VanishesOnWall eta ∧ H₁.wall = eta ∧ H₂.wall = eta ∧ DistBoundedInHalfApartment af eta S H₁ ∧ DistUnboundedInHalfApartment af eta S H₂

Given a sector $S$ and wall $\eta$, there exists an affine functional vanishing on $\eta$ that is bounded on one half-apartment and unbounded on the other.

theorem AffineBuilding.not_bounded_above_of_bounded_below_and_unbounded {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) (hbelow : BoundedBelowOn eta.functional S.vertices) : ¬BoundedAboveOn eta.functional S.vertices

Contrapositive corollary of Wall.sector_unbounded: bounded below implies not bounded above.

theorem AffineBuilding.not_bounded_below_of_bounded_above_and_unbounded {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) (habove : BoundedAboveOn eta.functional S.vertices) : ¬BoundedBelowOn eta.functional S.vertices

Symmetric corollary: bounded above implies not bounded below.

theorem AffineBuilding.exists_vertex_above {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (f : V → ℝ) (hnot_above : ¬BoundedAboveOn f S.vertices) (M : ℝ) : ∃ v ∈ S.vertices, M < f v

An unbounded-above function attains arbitrarily large values on the sector.

theorem AffineBuilding.exists_vertex_below {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (f : V → ℝ) (hnot_below : ¬BoundedBelowOn f S.vertices) (M : ℝ) : ∃ v ∈ S.vertices, f v < M

An unbounded-below function attains arbitrarily small values on the sector.

theorem AffineBuilding.sector_subsector_in_half_apartment {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) : ∃ (H : HalfApartment b) (S' : Sector b), H.wall = eta ∧ Sector.Subsector b S' S ∧ ∀ v ∈ S'.vertices, v ∈ H.vertices

Every sector contains a subsector $S'$ lying entirely in one half-apartment of a given wall $\eta$ (Section 16.7).

def AffineBuilding.IsPositiveHalfApartment {V : Type} [DecidableEq V] {b : Building V} (S : Sector b) (eta : Wall b) (H : HalfApartment b) : Prop

$H$ is the positive half-apartment for $(S, \eta)$: $H.\text{wall} = \eta$ and some subsector of $S$ lies entirely in $H$.

theorem AffineBuilding.exists_positive_half_apartment {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (eta : Wall b) (heta_apt : eta.apartment = S.apartment) : ∃ (H : HalfApartment b), IsPositiveHalfApartment S eta H

For every sector $S$ and wall $\eta$ there is a positive half-apartment $H$.