The sample of an offspring field

def BranchingProcess.sample {N : ℕ} (c : Word N → ℕ) : Subtree N

The tree cut out of 𝒩(N) by a field c of offspring counts: the vertex v keeps its children v ++ [j] with j < c v, so a word belongs to the sample when every one of its steps is below the offspring count at the vertex it leaves. Prefix closure is immediate, a prefix imposing fewer conditions.

Equations

• BranchingProcess.sample c = ⟨{v : List (Fin N) | ∀ (i : ℕ) (h : i < v.length), ↑(v.get ⟨i, h⟩) < c (List.take i v)}, ⋯⟩

theorem BranchingProcess.mem_sample_iff {N : ℕ} {c : Word N → ℕ} {v : Word N} : v ∈ sample c ↔ ∀ (i : ℕ) (h : i < List.length v), ↑(List.get v ⟨i, h⟩) < c (List.take i v)

Membership in the sample, unfolded.

theorem BranchingProcess.mem_sample_iff' {N : ℕ} {c : Word N → ℕ} {v : Word N} : v ∈ sample c ↔ ∀ (i : ℕ) (h : i < List.length v), ↑v[i] < c (List.take i v)

The same condition indexed by getElem, the shape the proofs below consume.

@[simp]

theorem BranchingProcess.nil_mem_sample {N : ℕ} (c : Word N → ℕ) : [] ∈ sample c

The root belongs to every sample.

theorem BranchingProcess.mem_sample_append_singleton {N : ℕ} {c : Word N → ℕ} {v : Word N} {j : Fin N} : v ++ [j] ∈ sample c ↔ v ∈ sample c ∧ ↑j < c v

The one-step criterion. A child v ++ [j] lies in the sample exactly when its parent does and the offspring count at the parent exceeds j.

theorem BranchingProcess.singleton_mem_sample_iff {N : ℕ} {c : Word N → ℕ} {j : Fin N} : [j] ∈ sample c ↔ ↑j < c []

A one-letter word lies in the sample exactly when the root has that many children.

The branching property

theorem BranchingProcess.append_mem_sample_iff {N : ℕ} (c : Word N → ℕ) (v w : Word N) : v ++ w ∈ sample c ↔ v ∈ sample c ∧ w ∈ sample fun (u : Word N) => c (v ++ u)

Splitting a word at a vertex. A concatenation lies in the sample exactly when its head does and its tail lies in the sample of the field shifted to that head.

theorem BranchingProcess.subAt_sample {N : ℕ} {c : Word N → ℕ} {v : Word N} (hv : v ∈ sample c) : Descriptive.Tree.subAt (sample c) v = sample fun (w : Word N) => c (v ++ w)

The branching property. The residual subtree of a sample at one of its vertices is again a sample, for the offspring field shifted to that vertex. Every recursion below runs off this identity.

Decomposition at the root

theorem BranchingProcess.coe_sample {N : ℕ} (c : Word N → ℕ) : ↑(sample c) = {[]} ∪ ⋃ j ∈ {j : Fin N | ↑j < c []}, (fun (w : Word N) => [j] ++ w) '' ↑(sample fun (w : Word N) => c ([j] ++ w))

The decomposition at the root. A sample is its root together with the samples of the shifted fields hanging off the children of the root.

theorem BranchingProcess.finite_sample_of_forall_finite {N : ℕ} {c : Word N → ℕ} (h : ∀ (j : Fin N), ↑j < c [] → (↑(sample fun (w : Word N) => c ([j] ++ w))).Finite) : (↑(sample c)).Finite

Finiteness passes up to the root. A sample all of whose child samples are finite is finite: the root has at most N children, so the union is a finite one.

theorem BranchingProcess.exists_infinite_child_of_infinite {N : ℕ} {c : Word N → ℕ} (h : (↑(sample c)).Infinite) : ∃ (j : Fin N), ↑j < c [] ∧ (↑(sample fun (w : Word N) => c ([j] ++ w))).Infinite

The pigeonhole at the root. An infinite sample has a child whose sample is infinite.

Survival and the skeleton

def BranchingProcess.Survives {N : ℕ} (c : Word N → ℕ) : Prop

Survival of the sample of c: the tree it cuts out is infinite.

Equations

• BranchingProcess.Survives c = (↑(BranchingProcess.sample c)).Infinite

def BranchingProcess.skeleton {N : ℕ} (c : Word N → ℕ) : Set (Word N)

The skeleton of a sample: the vertices whose residual subtree is infinite, that is the vertices lying on an infinite ray.

Equations

• BranchingProcess.skeleton c = {v : BranchingProcess.Word N | v ∈ BranchingProcess.sample c ∧ (↑(Descriptive.Tree.subAt (BranchingProcess.sample c) v)).Infinite}

theorem BranchingProcess.mem_skeleton_iff {N : ℕ} {c : Word N → ℕ} {v : Word N} : v ∈ skeleton c ↔ v ∈ sample c ∧ (↑(Descriptive.Tree.subAt (sample c) v)).Infinite

Membership in the skeleton, unfolded.

theorem BranchingProcess.skeleton_subset_sample {N : ℕ} (c : Word N → ℕ) : skeleton c ⊆ ↑(sample c)

The skeleton is a set of vertices of the sample.

theorem BranchingProcess.nil_mem_skeleton_iff {N : ℕ} {c : Word N → ℕ} : [] ∈ skeleton c ↔ Survives c

The root lies in the skeleton exactly when the sample survives.

theorem BranchingProcess.exists_child_mem_skeleton {N : ℕ} {c : Word N → ℕ} {v : Word N} (hv : v ∈ skeleton c) : ∃ w ∈ v.children, w ∈ skeleton c

The skeleton has no leaves. A skeleton vertex has a child in the skeleton: its residual subtree is infinite and has finitely many child subtrees, so one of them is infinite.

Rays in the skeleton

theorem BranchingProcess.length_of_chain {N : ℕ} {r : ℕ → Word N} (hr : ∀ (n : ℕ), r (n + 1) ∈ (r n).children) (n : ℕ) : List.length (r n) = List.length (r 0) + n

Along a chain of children the lengths grow by one at each step.

theorem BranchingProcess.prefix_of_chain {N : ℕ} {r : ℕ → Word N} (hr : ∀ (n : ℕ), r (n + 1) ∈ (r n).children) {m n : ℕ} (h : m ≤ n) : r m <+: r n

A chain of children is increasing for the prefix order.

theorem BranchingProcess.treeDist_of_chain {N : ℕ} {r : ℕ → Word N} (hr : ∀ (n : ℕ), r (n + 1) ∈ (r n).children) (m n : ℕ) : treeDist (r m) (r n) = m.dist n

A chain of children is an isometric copy of ℕ inside 𝒩(N).

theorem BranchingProcess.exists_skeleton_ray {N : ℕ} {c : Word N → ℕ} {v : Word N} (hv : v ∈ skeleton c) : ∃ (r : ℕ → Word N), r 0 = v ∧ (∀ (n : ℕ), r n ∈ skeleton c) ∧ ∀ (n : ℕ), r (n + 1) ∈ (r n).children

Rays out of the skeleton. Every skeleton vertex starts an infinite ray of skeleton vertices. No compactness is needed: exists_child_mem_skeleton supplies the next vertex at each step, and the ray is the resulting recursion.

theorem BranchingProcess.exists_isometric_skeleton_ray {N : ℕ} {c : Word N → ℕ} {v : Word N} (hv : v ∈ skeleton c) : ∃ (r : ℕ → Word N), r 0 = v ∧ (∀ (n : ℕ), r n ∈ skeleton c) ∧ (∀ (n : ℕ), r (n + 1) ∈ (r n).children) ∧ ∀ (m n : ℕ), treeDist (r m) (r n) = m.dist n

The metric form of exists_skeleton_ray: the ray is an isometric copy of ℕ.