Words

@[reducible, inline]

abbrev BranchingProcess.Word (N : ℕ) : Type

A vertex of the ambient N-ary tree 𝒩(N): a finite word over the alphabet Fin N. The root is the empty word [], and the children of v are the words v ++ [j] with j : Fin N.

Equations

• BranchingProcess.Word N = List (Fin N)

theorem BranchingProcess.length_lt_of_prefix_ne {N : ℕ} {v w : Word N} (h : v <+: w) (hne : v ≠ w) : List.length v < List.length w

A proper prefix is shorter.

The longest common prefix

def BranchingProcess.wedge {N : ℕ} : Word N → Word N → Word N

The longest common prefix v ∧ w of two words: their wedge point in 𝒩(N).

Equations

• BranchingProcess.wedge [] x✝ = []
• BranchingProcess.wedge x✝ [] = []
• BranchingProcess.wedge (a :: v) (b :: w) = if a = b then a :: BranchingProcess.wedge v w else []

@[simp]

theorem BranchingProcess.wedge_nil_left {N : ℕ} (w : Word N) : wedge [] w = []

@[simp]

theorem BranchingProcess.wedge_nil_right {N : ℕ} (v : Word N) : wedge v [] = []

theorem BranchingProcess.wedge_cons_cons {N : ℕ} (a b : Fin N) (v w : Word N) : wedge (a :: v) (b :: w) = if a = b then a :: wedge v w else []

The recursion step of wedge: a common first letter is kept, a mismatch stops.

@[simp]

theorem BranchingProcess.wedge_self {N : ℕ} (v : Word N) : wedge v v = v

The wedge of a word with itself is that word.

theorem BranchingProcess.wedge_comm {N : ℕ} (v w : Word N) : wedge v w = wedge w v

The wedge is symmetric.

theorem BranchingProcess.wedge_prefix_left {N : ℕ} (v w : Word N) : wedge v w <+: v

The wedge is a prefix of its first argument.

theorem BranchingProcess.wedge_prefix_right {N : ℕ} (v w : Word N) : wedge v w <+: w

The wedge is a prefix of its second argument.

theorem BranchingProcess.prefix_wedge_of_prefix {N : ℕ} {u v w : Word N} (hv : u <+: v) (hw : u <+: w) : u <+: wedge v w

Maximality: the wedge is the greatest lower bound for the prefix order.

theorem BranchingProcess.wedge_of_prefix {N : ℕ} {v w : Word N} (h : v <+: w) : wedge v w = v

A word wedged with an extension of itself is unchanged.

theorem BranchingProcess.wedge_length_le_left {N : ℕ} (v w : Word N) : List.length (wedge v w) ≤ List.length v

theorem BranchingProcess.wedge_length_le_right {N : ℕ} (v w : Word N) : List.length (wedge v w) ≤ List.length w

theorem BranchingProcess.wedge_append_append {N : ℕ} (u v w : Word N) : wedge (u ++ v) (u ++ w) = u ++ wedge v w

Wedging commutes with a common prefix.

theorem BranchingProcess.wedge_length_add_le {N : ℕ} (u v w : Word N) : List.length (wedge u v) + List.length (wedge v w) ≤ List.length v + List.length (wedge u w)

Of the three wedges of a triple, the two shortest agree; in the form the triangle inequality consumes, |u ∧ v| + |v ∧ w| ≤ |v| + |u ∧ w|.

The metric of the ambient tree

def BranchingProcess.treeDist {N : ℕ} (v w : Word N) : ℕ

The graph metric of 𝒩(N): the path distance d(v,w) = |v| + |w| - 2|v ∧ w|.

Equations

• BranchingProcess.treeDist v w = List.length v + List.length w - 2 * List.length (BranchingProcess.wedge v w)

theorem BranchingProcess.two_mul_wedge_length_le {N : ℕ} (v w : Word N) : 2 * List.length (wedge v w) ≤ List.length v + List.length w

The subtraction defining treeDist does not truncate.

theorem BranchingProcess.treeDist_add {N : ℕ} (v w : Word N) : treeDist v w + 2 * List.length (wedge v w) = List.length v + List.length w

The truncation-free form of the metric.

theorem BranchingProcess.treeDist_comm {N : ℕ} (v w : Word N) : treeDist v w = treeDist w v

The metric is symmetric.

@[simp]

theorem BranchingProcess.treeDist_self {N : ℕ} (v : Word N) : treeDist v v = 0

theorem BranchingProcess.treeDist_eq_zero_iff {N : ℕ} {v w : Word N} : treeDist v w = 0 ↔ v = w

The metric separates points.

theorem BranchingProcess.treeDist_of_prefix {N : ℕ} {v w : Word N} (h : v <+: w) : treeDist v w = List.length w - List.length v

Along a chain of prefixes the metric is the difference of the lengths.

theorem BranchingProcess.treeDist_triangle {N : ℕ} (u v w : Word N) : treeDist u w ≤ treeDist u v + treeDist v w

The triangle inequality.

theorem BranchingProcess.treeDist_append_left {N : ℕ} (u v w : Word N) : treeDist (u ++ v) (u ++ w) = treeDist v w

A common prefix is an isometry onto the residual subtree it names.

Parents and children

def BranchingProcess.Word.children {N : ℕ} (v : Word N) : Set (Word N)

The children of v in 𝒩(N): the words obtained from v by appending one letter.

Equations

• v.children = {w : BranchingProcess.Word N | ∃ (j : Fin N), w = v ++ [j]}

@[simp]

theorem BranchingProcess.Word.mem_children {N : ℕ} {v w : Word N} : w ∈ v.children ↔ ∃ (j : Fin N), w = v ++ [j]

theorem BranchingProcess.Word.prefix_of_mem_children {N : ℕ} {v w : Word N} (h : w ∈ v.children) : v <+: w

A vertex is a prefix of each of its children.

@[simp]

theorem BranchingProcess.treeDist_append_singleton {N : ℕ} (v : Word N) (j : Fin N) : treeDist v (v ++ [j]) = 1

An edge of 𝒩(N) has length one.

theorem BranchingProcess.treeDist_of_mem_children {N : ℕ} {v w : Word N} (h : w ∈ v.children) : treeDist v w = 1

Children sit at distance one from their parent.

Subtrees

@[reducible, inline]

abbrev BranchingProcess.Subtree (N : ℕ) : Type

A subtree of 𝒩(N): a prefix-closed set of words, taken as a term of Descriptive.tree (Fin N). That type carries the SetLike membership v ∈ T and the complete-lattice structure on prefix-closed sets, so intersections, unions and the extreme elements come for free.

Equations

• BranchingProcess.Subtree N = ↥(Descriptive.tree (Fin N))

theorem BranchingProcess.Subtree.mem_of_prefix {N : ℕ} {T : Subtree N} {v w : Word N} (h : v <+: w) (hw : w ∈ T) : v ∈ T

Prefix closure, in the notation of 𝒩(N).

theorem BranchingProcess.Subtree.nil_mem {N : ℕ} {T : Subtree N} {v : Word N} (hv : v ∈ T) : [] ∈ T

A subtree with a vertex contains the root.

theorem BranchingProcess.Subtree.mem_of_mem_children {N : ℕ} {T : Subtree N} {v w : Word N} (hw : w ∈ v.children) (h : w ∈ T) : v ∈ T

The parent of a vertex of T lies in T.

theorem BranchingProcess.Subtree.wedge_mem {N : ℕ} {T : Subtree N} {v : Word N} (hv : v ∈ T) (w : Word N) : wedge v w ∈ T

The wedge of a vertex of a subtree with any word is again a vertex of it: subtrees are closed under the meet of 𝒩(N).

theorem BranchingProcess.Subtree.mem_subAt {N : ℕ} {T : Subtree N} {v w : Word N} : w ∈ Descriptive.Tree.subAt T v ↔ v ++ w ∈ T

The residual subtree at a node v, Descriptive.Tree.subAt, read off in the notation of 𝒩(N): it consists of the words w with v ++ w in T.

theorem BranchingProcess.Subtree.nil_mem_subAt {N : ℕ} {T : Subtree N} {v : Word N} (hv : v ∈ T) : [] ∈ Descriptive.Tree.subAt T v

The residual subtree at a vertex of T contains the root.

theorem BranchingProcess.Subtree.append_mem_of_prefix {N : ℕ} {T : Subtree N} {v x y : Word N} (h : x <+: y) (hy : v ++ y ∈ T) : v ++ x ∈ T

Prefix closure of the residual subtree, in the unfolded form a Galton-Watson recursion consumes: shortening the tail of a vertex of T below v stays in T.