Galton–Watson branching processes in Lean

4 The Harris decomposition

Conditioned on survival, the skeleton of a Galton–Watson tree is again a Galton–Watson tree, for a reduced law, and the subtrees hanging off it are independent Galton–Watson trees for a conjugate law. This chapter proves both halves and then their joint form.