A guide to the notation
Definitions, from the paper to Lean
The closed unit ball, the topology of K, and the coefficient space enter through separate definitions. The excerpts below are taken directly from the Lean source files.
The closed unit ball
BX = {x ∈ X : ‖x‖ ≤ 1} carries the metric inherited from the ambient normed space. The Lean subtype includes the norm bound with each point, so a self-map of UnitBall X already has the correct domain and range.
abbrev UnitBall (X : Type u) [SeminormedAddCommGroup X] := {x : X // ‖x‖ ≤ 1}Context: namespace BFPP; universe u
The ball fixed point property
Every nonexpansive self-map of the closed unit ball has a fixed point. LipschitzWith 1 T means that distances do not increase.
The equivalent formulation for all closed balls, including radius zero, is proved in BallScaling.lean.
def HasBFPP (X : Type u) [SeminormedAddCommGroup X] : Prop :=
∀ T : UnitBall X → UnitBall X, LipschitzWith 1 T → ∃ x, T x = xContext: namespace BFPP; universe u
Compact F-spaces
For compact Hausdorff spaces, the formulation used here says that disjoint cozero sets have disjoint closures. A cozero set is the set where a continuous real function is nonzero.
The separate condition ExtremallyDisconnected K comes from mathlib: closures of open sets are open.
def IsFSpace (K : Type u) [TopologicalSpace K] : Prop :=
∀ f g : C(K, ℝ), Disjoint {t | f t ≠ 0} {t | g t ≠ 0} →
Disjoint (closure {t | f t ≠ 0}) (closure {t | g t ≠ 0})Context: namespace BFPP; open Set; universe u
Bounded coefficient families
The coefficient space is ℓ∞ on an index set, with the supremum norm. Giving the index set the discrete topology makes every function continuous; boundedness remains part of mathlib’s BoundedContinuousFunction structure.
This choice has no effect on the topology of K. The ordinal spaces used for C₀ synthesis carry their order topology separately.
abbrev BoundedFamily (ι : Type u) :=
@BoundedContinuousFunction ι ℝ ⊥ inferInstanceContext: namespace BFPP; universe u
An ordinal as an index set
OrdinalIndex κ is the type of ordinals strictly below κ. Thus a coefficient family has one coordinate for each stage of the transfinite recurrence.
abbrev OrdinalIndex (τ : Ordinal.{u}) := Set.Iio τContext: namespace BFPP; universe u
A transfinite contractive propagator
A map 𝒫 : 𝒟 → 𝒟 is governed by its earlier coordinates:
- The initial output coordinate is constant.
- At each successor, the output is a nonexpansive function of the input prefix that actually occurs in 𝒟.
- At each nonzero limit, the output is the upper or lower tail envelope of that prefix; the choice is fixed independently of the input.
inputPrefix restricts a family to the earlier coordinates, and prefixLift regards that prefix as a member of the actual range. IsSuccLimit is Lean’s nonzero limit condition.
These local rules imply global nonexpansiveness, proved by IsTCP.nonexpansive in the same module. Excluding fixed points requires the additional comparison argument.
structure IsTCP (D : Set (BoundedFamily (OrdinalIndex κ))) (P : D → D) : Prop where
positive : 0 < κ
nonempty : D.Nonempty
at_zero : ∃ c : ℝ, ∀ x, (P x).val ⟨0, positive⟩ = c
successor_rules : ∀ i : OrdinalIndex κ, i.val ∈ range (Order.succ : Ordinal.{u} → Ordinal.{u}) →
∃ Φ : range (inputPrefix D i) → ℝ, LipschitzWith 1 Φ ∧
∀ x, Φ (prefixLift D i x) = (P x).val i
limit_rules : ∀ i : OrdinalIndex κ, IsSuccLimit i.val →
∃ ε : Bool, ∀ x, (P x).val i =
if ε then upperEnvelope (inputPrefix D i x) else lowerEnvelope (inputPrefix D i x)Context: namespace BFPP; open Set Order; universe u; κ : Ordinal.{u}
Further definitions
The tail envelopes, profiles and delay, and two-profile domain are available with their full proofs in the source browser.