Well-founded descriptive trees, ordinal ranks, and analytic boundedness

A descriptive tree T : Descriptive.tree A (a prefix-closed set of finite sequences in List A) is well-founded (Descriptive.Tree.IsWellFounded T) when its immediate-extension relation Descriptive.Tree.ChildRel T has no infinite descending chain—equivalently, when T has no infinite branch f : ℕ → A all of whose initial segments List.ofFn (fun i : Fin n => f i) lie in T.

Each well-founded tree carries a canonical ordinal rank Descriptive.Tree.rank T in the universe of A, defined from Acc.rank under T.ChildRel as ⨆ u : T, Order.succ (h.apply u).rank (and 0 on ⊥ or on ill-founded trees). When [] ∈ T, the root has the largest node rank in T, yielding the standard subtree recursion rank T = Order.succ (⨆ a : A, rank (subAt T [a])) (Descriptive.Tree.IsWellFounded.rank_eq_succ_iSup), and more generally at any node x ∈ T via Mathlib's residual tree Descriptive.Tree.subAt T x. Over a countable alphabet A, every well-founded tree on A has countable rank (rank T < ω₁).

The main theorem is the Lusin–Sierpiński / Kunen–Martin boundedness theorem for analytic families of well-founded trees (MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one): if s ⊆ X is analytic and F : X → Descriptive.tree A over a countable alphabet A assigns a well-founded tree to each x ∈ s so that {x : s | u ∈ F x.1} is closed in s for every finite sequence u : List A, then some countable ordinal β < ω₁ strictly bounds rank (F x) across all x ∈ s. Only relative closedness of node membership (upper semicontinuity), not clopenness, is needed: pulling an unbounded family back along a continuous surjection (ℕ → ℕ) → s produces nested Baire cylinders and a sequence f : ℕ → A whose initial segments belong to trees at parameters converging to a limit z*, so closedness places the entire infinite branch in the tree at z*.

Main definitions

• Descriptive.Tree.ChildRel: immediate one-element extension on the nodes of a descriptive tree.
• Descriptive.Tree.IsWellFounded: well-foundedness of ChildRel on a descriptive tree.
• Descriptive.Tree.rank: ordinal rank of a descriptive tree (0 on ⊥ and on ill-founded trees).

Main results

• Descriptive.Tree.isWellFounded_iff_forall_exists_notMem and Descriptive.Tree.not_isWellFounded_iff: a tree is well-founded iff every f : ℕ → A has a finite prefix outside T.
• Descriptive.Tree.IsWellFounded.rank_eq_succ_iSup and Descriptive.Tree.IsWellFounded.rank_subAt_eq_succ_iSup: the subtree recursion for rank.
• Descriptive.Tree.IsWellFounded.rank_lt_omega_one: on a countable alphabet, every well-founded tree has rank strictly below ω₁.
• Descriptive.Tree.exists_rank_lt_omega_one_of_nat_nat: boundedness below ω₁ for families of well-founded trees indexed by Baire space ℕ → ℕ with closed node-membership sets.
• MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one and MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one_of_isClosed: boundedness below ω₁ for analytic families of well-founded trees.

References

• Alexander S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Sections 2.B and 2.E (well-founded trees and their ranks) and Theorem 31.1 (boundedness for analytic sets of well-founded trees).
• The Baire-cylinder descent for analytic families of well-founded trees also appears in Cameron Freer's cameronfreer/infinitary-logic (checkpoint 518a366cba97b1ae8c4dc64a297a396939bc3e0b, Apache-2.0), InfinitaryLogic/Descriptive/BFSeparation.lean; here it is proved as a general theorem for Descriptive.tree A over an arbitrary countable alphabet A assuming only relative closedness of node-membership sets.

Immediate extensions and well-foundedness

def Descriptive.Tree.ChildRel {A : Type u} (T : ↥(tree A)) (v u : ↥T) : Prop

Immediate one-element extension on the nodes of a descriptive tree T: ChildRel T v u holds when v is obtained by appending a single symbol to u.

@[simp]

theorem Descriptive.Tree.childRel_iff {A : Type u} {T : ↥(tree A)} {v u : ↥T} : ChildRel T v u ↔ ∃ (a : A), ↑v = ↑u ++ [a]

Unfolding lemma for Descriptive.Tree.ChildRel.

def Descriptive.Tree.IsWellFounded {A : Type u} (T : ↥(tree A)) : Prop

A descriptive tree T is well-founded when its immediate-extension relation ChildRel T is well-founded (equivalently, T has no infinite branch).

theorem Descriptive.Tree.isWellFounded_iff {A : Type u} {T : ↥(tree A)} : IsWellFounded T ↔ WellFounded (ChildRel T)

Unfolding lemma for Descriptive.Tree.IsWellFounded.

theorem Descriptive.Tree.IsWellFounded.apply {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) (u : ↥T) : Acc (ChildRel T) u

Every node of a well-founded descriptive tree is accessible under ChildRel.

@[simp]

theorem Descriptive.Tree.isWellFounded_bot {A : Type u} : IsWellFounded ⊥

The empty tree is well-founded.

theorem Descriptive.Tree.IsWellFounded.mono {A : Type u} {S T : ↥(tree A)} (hST : S ≤ T) (hT : IsWellFounded T) : IsWellFounded S

A subtree of a well-founded tree is well-founded.

theorem Descriptive.Tree.IsWellFounded.subAt {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) (x : List A) : IsWellFounded (Tree.subAt T x)

Every residual subtree Tree.subAt T x of a well-founded tree is well-founded.

theorem Descriptive.Tree.IsWellFounded.exists_notMem {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) (f : ℕ → A) : ∃ (n : ℕ), (List.ofFn fun (i : Fin n) => f ↑i) ∉ T

A well-founded tree admits no infinite branch: every sequence f : ℕ → A has a finite initial segment outside T.

theorem Descriptive.Tree.not_isWellFounded_iff {A : Type u} {T : ↥(tree A)} : ¬IsWellFounded T ↔ ∃ (f : ℕ → A), ∀ (n : ℕ), (List.ofFn fun (i : Fin n) => f ↑i) ∈ T

Infinite-branch characterization of ill-foundedness. A descriptive tree fails to be well-founded precisely when some f : ℕ → A has every finite initial segment in T.

theorem Descriptive.Tree.isWellFounded_iff_forall_exists_notMem {A : Type u} {T : ↥(tree A)} : IsWellFounded T ↔ ∀ (f : ℕ → A), ∃ (n : ℕ), (List.ofFn fun (i : Fin n) => f ↑i) ∉ T

Infinite-branch characterization of well-foundedness. A descriptive tree is well-founded precisely when every f : ℕ → A has a finite initial segment outside T.

Ordinal rank of a descriptive tree

noncomputable def Descriptive.Tree.rank {A : Type u} (T : ↥(tree A)) : Ordinal.{u}

The ordinal rank of a descriptive tree T on A: for a well-founded tree, the supremum of Order.succ of the ChildRel-ranks of its nodes (0 when T = ⊥), and 0 if T is not well-founded.

theorem Descriptive.Tree.rank_of_not_isWellFounded {A : Type u} {T : ↥(tree A)} (h : ¬IsWellFounded T) : rank T = 0

An ill-founded tree has rank 0 by convention.

theorem Descriptive.Tree.IsWellFounded.rank_eq_iSup {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) : rank T = ⨆ (u : ↥T), Order.succ ⋯.rank

On a well-founded tree, rank T unfolds to the supremum of successor node ranks.

@[simp]

theorem Descriptive.Tree.rank_bot {A : Type u} : rank ⊥ = 0

The empty tree has rank 0.

theorem Descriptive.Tree.rank_eq_zero_of_notMem {A : Type u} {T : ↥(tree A)} (h : [] ∉ T) : rank T = 0

Any tree not containing the root [] is empty and therefore has rank 0.

theorem Descriptive.Tree.rank_subAt_eq_zero_of_notMem {A : Type u} {T : ↥(tree A)} {x : List A} (h : x ∉ T) : rank (subAt T x) = 0

A residual subtree Tree.subAt T x at a sequence x ∉ T is empty and therefore has rank 0.

theorem Descriptive.Tree.IsWellFounded.rank_pos {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) (h : [] ∈ T) : 0 < rank T

A nonempty well-founded tree has positive rank.

theorem Descriptive.Tree.IsWellFounded.rank_subAt_pos {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) {x : List A} (hx : x ∈ T) : 0 < rank (Tree.subAt T x)

At any node x ∈ T of a well-founded tree, the residual subtree Tree.subAt T x has positive rank.

@[simp]

theorem Descriptive.Tree.IsWellFounded.rank_eq_zero_iff {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) : rank T = 0 ↔ T = ⊥

A well-founded tree has rank 0 iff it is empty.

theorem Descriptive.Tree.IsWellFounded.rank_eq_succ_iSup {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) (h : [] ∈ T) : rank T = Order.succ (⨆ (a : A), rank (Tree.subAt T [a]))

Subtree recursion at the root. On a nonempty well-founded tree T, the rank of T is the successor of the supremum of the ranks of its immediate residual subtrees Tree.subAt T [a].

theorem Descriptive.Tree.IsWellFounded.rank_subAt_eq_succ_iSup {A : Type u} {T : ↥(tree A)} (hT : IsWellFounded T) {x : List A} (hx : x ∈ T) : rank (Tree.subAt T x) = Order.succ (⨆ (a : A), rank (Tree.subAt T (x ++ [a])))

Subtree recursion at any node. On a well-founded tree T, for every x ∈ T the rank of Tree.subAt T x is the successor of the supremum of the ranks of Tree.subAt T (x ++ [a]).

theorem Descriptive.Tree.IsWellFounded.rank_mono {A : Type u} {S T : ↥(tree A)} (hST : S ≤ T) (hT : IsWellFounded T) : rank S ≤ rank T

Tree rank is monotone among subtrees of a well-founded tree.

theorem Descriptive.Tree.IsWellFounded.rank_lt_omega_one {A : Type u} {T : ↥(tree A)} [Countable A] (hT : IsWellFounded T) : rank T < Ordinal.omega 1

Countable-alphabet bound. Every well-founded descriptive tree over a countable alphabet A has ordinal rank strictly below ω₁.

Boundedness for Baire-indexed and analytic families of well-founded trees

theorem Descriptive.Tree.exists_rank_lt_omega_one_of_nat_nat {A : Type u} [Countable A] (F : (ℕ → ℕ) → ↥(tree A)) (hwf : ∀ (z : ℕ → ℕ), IsWellFounded (F z)) (hcl : ∀ (u : List A), IsClosed {z : ℕ → ℕ | u ∈ F z}) : ∃ β < Ordinal.omega 1, ∀ (z : ℕ → ℕ), rank (F z) < β

Boundedness on Baire space. Let F : (ℕ → ℕ) → tree A be a family of well-founded trees over a countable alphabet A such that {z | u ∈ F z} is closed in ℕ → ℕ for every finite sequence u : List A. Then some countable ordinal β < ω₁ strictly bounds rank (F z) across all z : ℕ → ℕ.

theorem MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one {X : Type u_1} [TopologicalSpace X] {A : Type u} [Countable A] {s : Set X} (hs : AnalyticSet s) (F : X → ↥(Descriptive.tree A)) (hwf : ∀ x ∈ s, Descriptive.Tree.IsWellFounded (F x)) (hcl : ∀ (u : List A), IsClosed {x : ↑s | u ∈ F ↑x}) : ∃ β < Ordinal.omega 1, ∀ x ∈ s, Descriptive.Tree.rank (F x) < β

Lusin–Sierpiński / Kunen–Martin boundedness theorem (relative form). Let s be an analytic subset of a topological space X and F : X → Descriptive.tree A a family of descriptive trees over a countable alphabet A : Type u. Suppose F x is well-founded for every x ∈ s and {x : s | u ∈ F x.1} is closed in the subspace s for every finite sequence u : List A. Then some countable ordinal β < ω₁ strictly bounds rank (F x) across all x ∈ s.

theorem MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one_of_isClosed {X : Type u_1} [TopologicalSpace X] {A : Type u} [Countable A] {s : Set X} (hs : AnalyticSet s) (F : X → ↥(Descriptive.tree A)) (hwf : ∀ x ∈ s, Descriptive.Tree.IsWellFounded (F x)) (hcl : ∀ (u : List A), IsClosed {x : X | u ∈ F x}) : ∃ β < Ordinal.omega 1, ∀ x ∈ s, Descriptive.Tree.rank (F x) < β

Lusin–Sierpiński / Kunen–Martin boundedness theorem (ambient-closed form). If s ⊆ X is analytic, F x is well-founded for every x ∈ s, and {x : X | u ∈ F x} is closed in X for every finite sequence u : List A, then some countable ordinal β < ω₁ strictly bounds rank (F x) across all x ∈ s.