Galton–Watson branching processes in Lean

4.2 The two halves

Theorem 4.4 The skeleton is a Galton–Watson tree
✓

If \(J\leq N\) and \(q{\lt}1\), the re-addressed skeleton of a sample conditioned on survival has the law of the Galton–Watson tree of the reduced law.

Proof ▶

Re-address the skeleton by giving the \(m\)-th surviving child of each skeleton vertex the letter \(m\). Under the law conditioned on survival, lemma 4.2 shows that the number of children of the root has law \(\tilde\theta \). Conditional on this number, the corresponding shifted fields are independent and each has the original law conditioned on survival.

We apply this root identity recursively to a finite prefix-closed set \(F\) of skeleton addresses. Induction on the maximal length of a word in \(F\) gives the same probability for the containment event \(\{ S\colon F\subseteq S\} \) under the re-addressed skeleton law and the Galton–Watson law with offspring distribution \(\tilde\theta \). Replacing a finite set of words by its prefix closure does not change this event for subtrees. These containment events form a \(\pi \)-system that generates the measurable space of subtrees, so uniqueness of probability measures proves the equality of laws.

Theorem 4.5 The bushes are Galton–Watson trees
✓

If \(J\leq N\) and \(q{\gt}0\), a sample conditioned on extinction has the law of the Galton–Watson tree of the conjugate law.

Proof ▶

Conditioned on extinction, the root can have \(j\) children only when all \(j\) shifted subfields become extinct. The branching property and independence therefore give

\[ \mathbb {P}^{\mathrm b}(c(\emptyset )=j) =\frac{\theta _jq^j}{q}=\hat\theta _j. \]

Conditional on this root count, the \(j\) shifted fields are independent and each has law \(\mathbb {P}^{\mathrm b}\). Recursing over a finite prefix-closed set of addresses shows that the bush law and the Galton–Watson law with offspring distribution \(\hat\theta \) agree on every finite containment event. As in the proof of theorem 4.4, these events generate the measurable space of subtrees, which proves the equality of laws.