Galton–Watson branching processes in Lean

1 The ambient tree

The genealogy of a branching process is carried inside a fixed ambient tree, whose vertices are words. Nothing in this chapter is probabilistic.

Definition 1.1 The ambient \(N\)-ary tree
✓

Fix \(N\in \mathbb {N}\). A vertex of the ambient tree \(\mathcal{N}(N)\) is a finite word over the alphabet \(\{ 0,\dots ,N-1\} \); the root is the empty word \(\emptyset \) and the children of \(v\) are the words \(v j\) with \(j{\lt}N\). The wedge \(v\wedge w\) of two vertices is their longest common prefix, and the graph metric of \(\mathcal{N}(N)\) is

\[ d(v,w)=\lvert v \rvert +\lvert w \rvert -2\lvert v\wedge w \rvert . \]
Lemma 1.2 The wedge is the greatest common prefix
✓

The wedge \(v\wedge w\) is a prefix of both \(v\) and \(w\), and every common prefix of \(v\) and \(w\) is a prefix of \(v\wedge w\).

Proof ▶

We first prove that \(v\wedge w\) is a prefix of \(v\) by induction on \(v\), splitting according to whether \(w\) is empty and, when both words are nonempty, whether their first letters agree. The corresponding assertion for \(w\) follows by symmetry. For maximality, we induct on a common prefix \(u\). If \(u\) is nonempty, the prefix assumptions force \(v\) and \(w\) to have the same first letter as \(u\), and the claim reduces to their tails.

The subtraction defining \(d\) does not truncate, \(d(v,w)=0\) exactly when \(v=w\), and \(d\) satisfies the triangle inequality. A vertex and one of its children are at distance one.

Proof ▶

Since \(v\wedge w\) is a prefix of both words, its length is bounded by each of \(\lvert v \rvert \) and \(\lvert w \rvert \). Thus \(2\lvert v\wedge w \rvert \leq \lvert v \rvert +\lvert w \rvert \), so the subtraction in the definition of \(d\) does not truncate. If \(d(v,w)=0\), these two length bounds are equalities. A prefix of the same length as a word is the word itself, which gives \(v=v\wedge w=w\).

For the triangle inequality, compare the two prefixes \(u\wedge v\) and \(v\wedge w\) of \(v\). One is a prefix of the other, and the shorter one is consequently a common prefix of \(u\) and \(w\). Hence

\[ \lvert u\wedge v \rvert +\lvert v\wedge w \rvert \leq \lvert v \rvert +\lvert u\wedge w \rvert . \]

Substituting this bound into the three distance formulae gives \(d(u,w)\leq d(u,v)+d(v,w)\). Finally, if \(w\) is a child of \(v\), then \(v\) is a prefix of \(w\) and \(\lvert w \rvert =\lvert v \rvert +1\), so \(d(v,w)=1\).

Definition 1.4 Subtrees
✓
#

A subtree of \(\mathcal{N}(N)\) is a prefix-closed set of words, taken as a term of Mathlib’s Descriptive.tree. The residual subtree of \(T\) at \(v\) is \(T_v=\{ w : vw\in T\} \).