The finite tree

The finite-height tree, its cylinder sets, and the parent-disjointness lemma.

@[reducible, inline]

abbrev OrderClosures.TreeNode (n : ℕ) : Type

Nodes of the finite-height tree G_n = ⋃_{k ≤ n} ℕ^k.

Equations

• OrderClosures.TreeNode n = { t : List ℕ // t.length ≤ n }

@[reducible, inline]

abbrev OrderClosures.TreeNode.level {n : ℕ} (t : TreeNode n) : ℕ

Level of a node.

Equations

• t.level = (↑t).length

def OrderClosures.TreeNode.root (n : ℕ) : TreeNode n

The root ∅.

Equations

• OrderClosures.TreeNode.root n = ⟨[], ⋯⟩

def OrderClosures.TreeNode.child {n : ℕ} (t : TreeNode n) (h : t.level < n) (m : ℕ) : TreeNode n

The child t⌢m.

Equations

• t.child h m = ⟨↑t ++ [m], ⋯⟩

def OrderClosures.TreeNode.parent {n : ℕ} (t : TreeNode n) : TreeNode n

The parent map, fixing the root.

Equations

• t.parent = ⟨(↑t).dropLast, ⋯⟩

def OrderClosures.TreeNode.restrict {n : ℕ} (t : TreeNode n) (j : ℕ) : TreeNode n

Restriction t|j.

Equations

• t.restrict j = ⟨List.take j ↑t, ⋯⟩

@[reducible, inline]

abbrev OrderClosures.TreeNonterminal (n : ℕ) : Type

Non-terminal nodes H_n.

Equations

• OrderClosures.TreeNonterminal n = { t : OrderClosures.TreeNode n // t.level < n }

@[reducible, inline]

abbrev OrderClosures.TreeProduct (n : ℕ) : Type

The product space I_n = ℕ^{H_n}.

Equations

• OrderClosures.TreeProduct n = (OrderClosures.TreeNonterminal n → ℕ)

def OrderClosures.strictPrefix {n : ℕ} (t : TreeNode n) (j : Fin t.level) : TreeNonterminal n

The strict prefix t|j, regarded as a non-terminal node.

Equations

• OrderClosures.strictPrefix t j = ⟨t.restrict ↑j, ⋯⟩

def OrderClosures.treeCylinder (n : ℕ) (t : TreeNode n) : Set (TreeProduct n)

The cylinder E_t.

Equations

• OrderClosures.treeCylinder n t = {α : OrderClosures.TreeProduct n | ∀ (j : Fin t.level), α (OrderClosures.strictPrefix t j) ≤ (↑t).get j}

theorem OrderClosures.mem_treeCylinder_child_iff (n : ℕ) (t : TreeNode n) (ht : t.level < n) (m : ℕ) (α : TreeProduct n) : α ∈ treeCylinder n (t.child ht m) ↔ α ∈ treeCylinder n t ∧ α ⟨t, ht⟩ ≤ m

Characterizes membership in a child cylinder by the parent coordinates and one new label; used in the cylinder partition proofs.

theorem OrderClosures.treeCylinder_isClopen (n : ℕ) (t : TreeNode n) : IsClopen (treeCylinder n t)

Paper Lemma lem:basic-tree, part (a).

noncomputable def OrderClosures.treeFunction (n : ℕ) (t : TreeNode n) : BoundedContinuousFunction (TreeProduct n) ℝ

The characteristic function s_t = χ_{E_t}.

Equations

• OrderClosures.treeFunction n t = BoundedContinuousFunction.indicator (OrderClosures.treeCylinder n t) ⋯

theorem OrderClosures.treeFunction_apply_of_mem (n : ℕ) (t : TreeNode n) {α : TreeProduct n} (hα : α ∈ treeCylinder n t) : (treeFunction n t) α = 1

Evaluates a tree function on its supporting cylinder; used in the exact basis and tree-operator computations.

theorem OrderClosures.treeFunction_apply_of_notMem (n : ℕ) (t : TreeNode n) {α : TreeProduct n} (hα : α ∉ treeCylinder n t) : (treeFunction n t) α = 0

Evaluates a tree function off its supporting cylinder; used to show finite tree sums vanish outside their cylinder union.

@[instance_reducible]

noncomputable instance OrderClosures.boundedContinuousFunctionNormedVectorLattice (A : Type u) [TopologicalSpace A] : NormedVectorLattice (BoundedContinuousFunction A ℝ)

BanLat's vector-lattice structure is supplied here for real-valued bounded continuous functions; all non-proof data comes from Mathlib's pointwise instances.

Equations

• OrderClosures.boundedContinuousFunctionNormedVectorLattice A = { toModule := BoundedContinuousFunction.instModule, toPosSMulMono := ⋯, toHasSolidNorm := ⋯, toNormSMulClass := ⋯ }

theorem OrderClosures.treeFunction_child_properties (n : ℕ) (t : TreeNode n) (ht : t.level < n) : (∀ (m : ℕ), treeCylinder n (t.child ht m) ⊆ treeCylinder n t ∧ treeFunction n (t.child ht m) ≤ treeFunction n t) ∧ (Monotone fun (m : ℕ) => treeFunction n (t.child ht m)) ∧ IsLUB (Set.range fun (m : ℕ) => treeFunction n (t.child ht m)) (treeFunction n t)

Paper Lemma lem:basic-tree, parts (b) and (c).

theorem OrderClosures.treeCylinder_finite_cover (n : ℕ) (t : TreeNode n) (F : Finset (TreeNode n)) (hcover : ∀ α ∈ treeCylinder n t, ∃ u ∈ F, α ∈ treeCylinder n u) : ∃ u ∈ F, treeCylinder n t ⊆ treeCylinder n u

Paper Lemma lem:finite-cover.

def OrderClosures.ParentDisjoint {n : ℕ} (A B : Set (TreeNode n)) : Prop

Parent-disjointness (π-disjointness in the source).

Equations

• OrderClosures.ParentDisjoint A B = (OrderClosures.TreeNode.parent '' A ∩ OrderClosures.TreeNode.parent '' B = ∅)

def OrderClosures.finiteCylinderUnion (n : ℕ) (F : Finset (TreeNode n)) : Set (TreeProduct n)

The finite union of the cylinders indexed by F.

Equations

• OrderClosures.finiteCylinderUnion n F = ⋃ (t : ↥F), OrderClosures.treeCylinder n ↑t

noncomputable def OrderClosures.finiteTreeSup (n : ℕ) (F : Finset (TreeNode n)) : BoundedContinuousFunction (TreeProduct n) ℝ

The finite supremum of the tree functions, represented by the indicator of the corresponding finite union.

Equations

• OrderClosures.finiteTreeSup n F = BoundedContinuousFunction.indicator (OrderClosures.finiteCylinderUnion n F) ⋯

def OrderClosures.treeLastLabel {n : ℕ} (t : TreeNode n) : ℕ

The last label of a nonroot node, with a harmless root default; used to construct coordinates escaping finite cylinder unions.

Equations

• OrderClosures.treeLastLabel t = if h : 0 < t.level then (↑t).get ⟨t.level - 1, ⋯⟩ else 0

theorem OrderClosures.strictPrefix_last_eq_parent {n : ℕ} (t : TreeNode n) (ht : 0 < t.level) : have j := ⟨t.level - 1, ⋯⟩; ↑(strictPrefix t j) = t.parent ∧ (↑t).get j = treeLastLabel t

Identifies the last strict prefix with the parent of a nonroot node; used when constructing points outside parent-disjoint cylinder families.

theorem OrderClosures.finiteTreeSup_nonneg (n : ℕ) (F : Finset (TreeNode n)) : 0 ≤ finiteTreeSup n F

Records positivity of a finite supremum of tree functions; used in the least-upper-bound statement for parent-disjoint families.

theorem OrderClosures.finiteTreeSup_apply_of_notMem (n : ℕ) (F : Finset (TreeNode n)) {α : TreeProduct n} (hα : α ∉ finiteCylinderUnion n F) : (finiteTreeSup n F) α = 0

Shows that a finite tree supremum vanishes outside its cylinder union; used in the common-lower-bound argument.

theorem OrderClosures.commonLower_le_zero_of_parentDisjoint_subseq (n : ℕ) (F : ℕ → Finset (TreeNode n)) (hF : Pairwise fun (i j : ℕ) => ParentDisjoint ↑(F i) ↑(F j)) (φ : ℕ → ℕ) (hφ : Function.Injective φ) (hroot : ∀ (m : ℕ), TreeNode.root n ∉ F (φ m)) (g : ℕ → BoundedContinuousFunction (TreeProduct n) ℝ) (hgzero : ∀ (m : ℕ), ∀ α ∉ finiteCylinderUnion n (F (φ m)), (g (φ m)) α = 0) {z : BoundedContinuousFunction (TreeProduct n) ℝ} (hz : ∀ (m : ℕ), z ≤ g m) : z ≤ 0

Forces a common lower bound to be nonpositive when supports have parent-disjoint subsequences; reused in both tree and transient-band lemmas.

theorem OrderClosures.parentDisjoint_treeFunctions_iInf (n : ℕ) (F : ℕ → Finset (TreeNode n)) (hF : Pairwise fun (i j : ℕ) => ParentDisjoint ↑(F i) ↑(F j)) : IsGLB (Set.range fun (m : ℕ) => finiteTreeSup n (F m)) 0

Paper Lemma lem:pi-disjoint.