Multitype Galton–Watson processes

A multitype Galton–Watson process with types ι is an offspring kernel ξ : Kernel ι (List ι): an individual of type i has offspring drawn from ξ i, an ordered list of types, each of which founds an independent copy of the process. The family tree of an individual is the plane tree of [Nev86], a RoseTree ι; its law on finite trees is the least fixed point of the one-generation operator on the Giry monad, and the missing mass is the probability of surviving forever.

A probabilistic context-free grammar is the instance whose types are the symbols: a terminal has no offspring, and a nonterminal's offspring is the right-hand side of a rule chosen with its weight; see PCFG.galtonWatson.

Main definitions

• GaltonWatson.PartialTree: family trees with holes, the states of the generation chain.
• GaltonWatson.fill: the kernel filling the holes of a partial tree with independent draws from a family of laws, and GaltonWatson.generation: the kernel expanding every hole by one generation.
• GaltonWatson.expand: one generation from a single hole followed by filling, and GaltonWatson.law: its least fixed point, the law of the finite family tree at each type.
• GaltonWatson.weight: the probability of a finite family tree, the product over its nodes of the offspring probability there.
• GaltonWatson.extinctionProb: the total mass of law, the probability that the family tree is finite.
• GaltonWatson.chainKernel, GaltonWatson.trajectory: with Markov offspring, the generation chain in Ionescu–Tulcea form and, through ProbabilityTheory.Kernel.traj, the law of its whole trajectory.

Main results

• GaltonWatson.law_eq_iSup_iterate: the law is the supremum of the Kleene iterates of expand from the zero kernel.
• GaltonWatson.law_singleton: a finite tree rooted at type i has probability weight under the law at i, and trees rooted elsewhere have probability 0.
• GaltonWatson.law_univ_le_one: with sub-probability offspring the law is a sub-probability kernel.
• GaltonWatson.fill_expand: filling with one more generation is one generation followed by filling, so GaltonWatson.fill_iterate identifies the Kleene iterates with the completed part of the generation chain and GaltonWatson.law_eq_iSup_generation expresses the law as their supremum.
• GaltonWatson.trajectory_map_eval: at time n the trajectory is distributed as n generations, so the Kleene iterates are the marginals of the trajectory measure.

Implementation notes

Trees and lists carry the discrete σ-algebra ⊤, so every function out of them is measurable and, with ι countable, every measure on them is s-finite and every kernel between them is an s-finite kernel; Fubini then needs no finiteness hypotheses. Partial trees are RoseTree (ι ⊕ ι), a hole of type i being a leaf Sum.inl i and an expanded individual a node Sum.inr i. The offspring kernel is not required to be Markov: sub-probability offspring model killing, and the grammar instance produces the zero measure at a nonterminal no rule expands. The extinction probability is the least fixed point of the offspring generating function and equals one exactly when the mean matrix is subcritical or critical ([AN72]); that theorem is not proved here.

References

• [Nev86]
• [AN72]

@[instance_reducible]

instance instMeasurableSpaceRoseTree {α : Type u_1} : MeasurableSpace (RoseTree α)

Equations

• instMeasurableSpaceRoseTree = ⊤

@[reducible, inline]

abbrev ProbabilityTheory.GaltonWatson.PartialTree (ι : Type u_2) : Type u_2

In a partial family tree a leaf Sum.inl i is a hole of type i, yet to be expanded, and a node Sum.inr i is an individual of type i whose offspring is known.

Equations

• ProbabilityTheory.GaltonWatson.PartialTree ι = RoseTree (ι ⊕ ι)

@[reducible, inline]

abbrev ProbabilityTheory.GaltonWatson.hole {ι : Type u_1} (i : ι) : PartialTree ι

The hole of type i.

Equations

• ProbabilityTheory.GaltonWatson.hole i = RoseTree.leaf (Sum.inl i)

Filling the holes

noncomputable def ProbabilityTheory.GaltonWatson.fill {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) : Kernel (PartialTree ι) (RoseTree ι)

Fill the holes of a partial tree with independent draws from the laws κ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.GaltonWatson.fillList {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) : Kernel (List (PartialTree ι)) (List (RoseTree ι))

Fill the holes of a list of partial trees independently.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.GaltonWatson.fill_inl {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) (i : ι) (cs : List (PartialTree ι)) : (fill κ) (RoseTree.node (Sum.inl i) cs) = κ i

@[simp]

theorem ProbabilityTheory.GaltonWatson.fill_hole {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) (i : ι) : (fill κ) (hole i) = κ i

theorem ProbabilityTheory.GaltonWatson.fill_inr {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) (i : ι) (cs : List (PartialTree ι)) : (fill κ) (RoseTree.node (Sum.inr i) cs) = MeasureTheory.Measure.map (RoseTree.node i) ((fillList κ) cs)

@[simp]

theorem ProbabilityTheory.GaltonWatson.fillList_apply {ι : Type u_1} [MeasurableSpace ι] (κ : Kernel ι (RoseTree ι)) (ss : List (PartialTree ι)) : (fillList κ) ss = MeasureTheory.Measure.listProd (List.map (⇑(fill κ)) ss)

theorem ProbabilityTheory.GaltonWatson.fill_univ_le_one {ι : Type u_1} [MeasurableSpace ι] {κ : Kernel ι (RoseTree ι)} [Countable ι] (hκ : ∀ (i : ι), (κ i) Set.univ ≤ 1) (s : PartialTree ι) : ((fill κ) s) Set.univ ≤ 1

theorem ProbabilityTheory.GaltonWatson.isProbabilityMeasure_fill {ι : Type u_1} [MeasurableSpace ι] {κ : Kernel ι (RoseTree ι)} [IsMarkovKernel κ] (s : PartialTree ι) : MeasureTheory.IsProbabilityMeasure ((fill κ) s)

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelPartialTreeRoseTreeFill {ι : Type u_1} [MeasurableSpace ι] {κ : Kernel ι (RoseTree ι)} [IsMarkovKernel κ] : IsMarkovKernel (fill κ)

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelListPartialTreeRoseTreeFillList {ι : Type u_1} [MeasurableSpace ι] {κ : Kernel ι (RoseTree ι)} [IsMarkovKernel κ] : IsMarkovKernel (fillList κ)

theorem ProbabilityTheory.GaltonWatson.fillList_map_hole_singleton_of_ne {ι : Type u_1} [MeasurableSpace ι] {κ : Kernel ι (RoseTree ι)} [Countable ι] (hκ : ∀ (i : ι) (c : RoseTree ι), c.value ≠ i → (κ i) {c} = 0) (js : List ι) (cs : List (RoseTree ι)) : List.map RoseTree.value cs ≠ js → ((fillList κ) (List.map hole js)) {cs} = 0

A list of subtrees whose root types do not spell out the holes has mass 0, for any family of laws concentrated on trees of the right type.

One generation

noncomputable def ProbabilityTheory.GaltonWatson.generation {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) : Kernel (PartialTree ι) (PartialTree ι)

In one synchronous generation every hole draws its offspring and becomes a node whose children are fresh holes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.GaltonWatson.generationList {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) : Kernel (List (PartialTree ι)) (List (PartialTree ι))

One synchronous generation on a list of partial trees.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ProbabilityTheory.GaltonWatson.generation_inl {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (i : ι) (cs : List (PartialTree ι)) : (generation ξ) (RoseTree.node (Sum.inl i) cs) = MeasureTheory.Measure.map (fun (js : List ι) => RoseTree.node (Sum.inr i) (List.map hole js)) (ξ i)

@[simp]

theorem ProbabilityTheory.GaltonWatson.generation_hole {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (i : ι) : (generation ξ) (hole i) = MeasureTheory.Measure.map (fun (js : List ι) => RoseTree.node (Sum.inr i) (List.map hole js)) (ξ i)

theorem ProbabilityTheory.GaltonWatson.generation_inr {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (i : ι) (cs : List (PartialTree ι)) : (generation ξ) (RoseTree.node (Sum.inr i) cs) = MeasureTheory.Measure.map (RoseTree.node (Sum.inr i)) ((generationList ξ) cs)

@[simp]

theorem ProbabilityTheory.GaltonWatson.generationList_apply {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (ss : List (PartialTree ι)) : (generationList ξ) ss = MeasureTheory.Measure.listProd (List.map (⇑(generation ξ)) ss)

theorem ProbabilityTheory.GaltonWatson.isProbabilityMeasure_generation {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] (s : PartialTree ι) : MeasureTheory.IsProbabilityMeasure ((generation ξ) s)

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelPartialTreeGenerationOfList {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] : IsMarkovKernel (generation ξ)

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelListPartialTreeGenerationList {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] : IsMarkovKernel (generationList ξ)

theorem ProbabilityTheory.GaltonWatson.fillList_comp_generationList {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] {κ : Kernel ι (RoseTree ι)} (ss : List (PartialTree ι)) : ((generationList ξ) ss).bind ⇑(fillList κ) = MeasureTheory.Measure.listProd (List.map (fun (s : PartialTree ι) => ((generation ξ) s).bind ⇑(fill κ)) ss)

Filling a list of partial trees after one generation on each.

noncomputable def ProbabilityTheory.GaltonWatson.expand {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (κ : Kernel ι (RoseTree ι)) : Kernel ι (RoseTree ι)

In one generation from a type i, a single hole of type i draws its offspring, and each type among them grows a family tree with law κ.

Equations

• ProbabilityTheory.GaltonWatson.expand ξ κ = ((ProbabilityTheory.GaltonWatson.fill κ).comp (ProbabilityTheory.GaltonWatson.generation ξ)).comap ProbabilityTheory.GaltonWatson.hole ⋯

@[simp]

theorem ProbabilityTheory.GaltonWatson.expand_apply {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] {κ : Kernel ι (RoseTree ι)} (i : ι) : (expand ξ κ) i = ((generation ξ) (hole i)).bind ⇑(fill κ)

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelRoseTreeExpandOfList {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] {κ : Kernel ι (RoseTree ι)} [IsMarkovKernel ξ] [IsMarkovKernel κ] : IsMarkovKernel (expand ξ κ)

theorem ProbabilityTheory.GaltonWatson.expand_apply' {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] {κ : Kernel ι (RoseTree ι)} (i : ι) (s : Set (RoseTree ι)) : ((expand ξ κ) i) s = ∫⁻ (js : List ι), ((fillList κ) (List.map hole js)) (RoseTree.node i ⁻¹' s) ∂ξ i

theorem ProbabilityTheory.GaltonWatson.fill_expand_apply {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] {κ : Kernel ι (RoseTree ι)} (s : PartialTree ι) : (fill (expand ξ κ)) s = ((generation ξ) s).bind ⇑(fill κ)

Filling with one more generation is one generation followed by filling.

theorem ProbabilityTheory.GaltonWatson.fill_expand {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] {κ : Kernel ι (RoseTree ι)} : fill (expand ξ κ) = (fill κ).comp (generation ξ)

Filling with one more generation is one generation followed by filling.

The weight of a finite family tree

noncomputable def ProbabilityTheory.GaltonWatson.weight {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (t : RoseTree ι) : ENNReal

The probability of a finite family tree is the product over its nodes of the offspring probability of the list of types below that node.

Equations

• ProbabilityTheory.GaltonWatson.weight ξ t = (List.map (fun (p : ι × List ι) => (ξ p.1) {p.2}) t.localTrees).prod

theorem ProbabilityTheory.GaltonWatson.weight_node {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (i : ι) (cs : List (RoseTree ι)) : weight ξ (RoseTree.node i cs) = (ξ i) {List.map RoseTree.value cs} * (List.map (weight ξ) cs).prod

The law of the family tree

theorem ProbabilityTheory.GaltonWatson.ωScottContinuous_fill {ι : Type u_1} [MeasurableSpace ι] [Countable ι] [MeasurableSingletonClass ι] (s : PartialTree ι) : OmegaCompletePartialOrder.ωScottContinuous fun (κ : ι → MeasureTheory.Measure (RoseTree ι)) => (fill (Kernel.ofFunOfCountable κ)) s

theorem ProbabilityTheory.GaltonWatson.ωScottContinuous_expand {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : OmegaCompletePartialOrder.ωScottContinuous fun (κ : ι → MeasureTheory.Measure (RoseTree ι)) => ⇑(expand ξ (Kernel.ofFunOfCountable κ))

noncomputable def ProbabilityTheory.GaltonWatson.expandHom {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : (ι → MeasureTheory.Measure (RoseTree ι)) →o ι → MeasureTheory.Measure (RoseTree ι)

The generation operator on families of laws indexed by type, as an order homomorphism.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.GaltonWatson.law {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : Kernel ι (RoseTree ι)

The law of the family tree of an individual of each type, on finite trees, is the least fixed point of the generation operator. Its total mass is the extinction probability.

Equations

• ProbabilityTheory.GaltonWatson.law ξ = ProbabilityTheory.Kernel.ofFunOfCountable (OrderHom.lfp (ProbabilityTheory.GaltonWatson.expandHom ξ))

theorem ProbabilityTheory.GaltonWatson.expand_law {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : expand ξ (law ξ) = law ξ

theorem ProbabilityTheory.GaltonWatson.coe_iterate_expand {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (n : ℕ) : ⇑((expand ξ)^[n] 0) = (⇑(expandHom ξ))^[n] ⊥

theorem ProbabilityTheory.GaltonWatson.law_eq_iSup_iterate {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : ⇑(law ξ) = ⨆ (n : ℕ), ⇑((expand ξ)^[n] 0)

The law is the supremum of the Kleene iterates of expand from the zero kernel.

theorem ProbabilityTheory.GaltonWatson.monotone_iterate_expand {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] : Monotone fun (n : ℕ) => ⇑((expand ξ)^[n] 0)

theorem ProbabilityTheory.GaltonWatson.law_singleton_of_ne {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] {t : RoseTree ι} {i : ι} (h : t.value ≠ i) : ((law ξ) i) {t} = 0

theorem ProbabilityTheory.GaltonWatson.fillList_law_map_hole_singleton {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] {cs : List (RoseTree ι)} (h : ∀ c ∈ cs, ((law ξ) c.value) {c} = weight ξ c) : ((fillList (law ξ)) (List.map hole (List.map RoseTree.value cs))) {cs} = (List.map (weight ξ) cs).prod

A list of family trees has probability the product of their weights below the holes it spells out, given the singleton law for each of them.

theorem ProbabilityTheory.GaltonWatson.law_singleton_value {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (t : RoseTree ι) : ((law ξ) t.value) {t} = weight ξ t

A family tree of an individual of type i has probability weight under the law at i.

theorem ProbabilityTheory.GaltonWatson.law_singleton_node {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (i : ι) (cs : List (RoseTree ι)) : ((law ξ) i) {RoseTree.node i cs} = weight ξ (RoseTree.node i cs)

theorem ProbabilityTheory.GaltonWatson.law_singleton {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (t : RoseTree ι) (i : ι) : ((law ξ) i) {t} = if t.value = i then weight ξ t else 0

Under the law at i, a finite tree has probability weight when its root has type i and 0 otherwise.

Extinction

theorem ProbabilityTheory.GaltonWatson.expand_univ_le_one {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] (hξ : ∀ (i : ι), (ξ i) Set.univ ≤ 1) {κ : Kernel ι (RoseTree ι)} (hκ : ∀ (i : ι), (κ i) Set.univ ≤ 1) (i : ι) : ((expand ξ κ) i) Set.univ ≤ 1

theorem ProbabilityTheory.GaltonWatson.iterate_expand_univ_le_one {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] (hξ : ∀ (i : ι), (ξ i) Set.univ ≤ 1) (n : ℕ) (i : ι) : (((expand ξ)^[n] 0) i) Set.univ ≤ 1

theorem ProbabilityTheory.GaltonWatson.law_univ_le_one {ι : Type u_1} [MeasurableSpace ι] {ξ : Kernel ι (List ι)} [Countable ι] [MeasurableSingletonClass ι] (hξ : ∀ (i : ι), (ξ i) Set.univ ≤ 1) (i : ι) : ((law ξ) i) Set.univ ≤ 1

With sub-probability offspring, the law on finite family trees is a sub-probability kernel; the missing mass is the probability of survival forever.

noncomputable def ProbabilityTheory.GaltonWatson.extinctionProb {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (i : ι) : ENNReal

The extinction probability of an individual of type i is the total mass of the law on finite family trees, which for Markov offspring is the probability that the family tree is finite.

Equations

• ProbabilityTheory.GaltonWatson.extinctionProb ξ i = ((ProbabilityTheory.GaltonWatson.law ξ) i) Set.univ

Generations

theorem ProbabilityTheory.GaltonWatson.fill_iterate {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (n : ℕ) : fill ((expand ξ)^[n] 0) = (fill 0).comp (generation ξ ^ n)

The n-th Kleene iterate fills a partial tree exactly as n synchronous generations do, followed by the completion of what remains.

theorem ProbabilityTheory.GaltonWatson.law_eq_iSup_generation {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [MeasurableSingletonClass ι] (i : ι) : (law ξ) i = ⨆ (n : ℕ), ((generation ξ ^ n) (hole i)).bind ⇑(fill 0)

The law of the family tree at type i is the supremum over n of the completed part of n synchronous generations from a single hole of type i.

The generation chain as a Markov chain

noncomputable def ProbabilityTheory.GaltonWatson.chainKernel {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) (n : ℕ) : Kernel ((i : ↥(Finset.Iic n)) → (fun (x : ℕ) => PartialTree ι) ↑i) ((fun (x : ℕ) => PartialTree ι) (n + 1))

In the Ionescu–Tulcea form of the generation chain, the state at time n + 1 depends on the trajectory up to time n only through its last coordinate.

Equations

• One or more equations did not get rendered due to their size.

instance ProbabilityTheory.GaltonWatson.instIsMarkovKernelForallPartialTreeValNatMemFinsetIicHAddOfNatChainKernel {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] (n : ℕ) : IsMarkovKernel (chainKernel ξ n)

noncomputable def ProbabilityTheory.GaltonWatson.chainTraj {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] (n : ℕ) : Kernel ((i : ↥(Finset.Iic n)) → (fun (x : ℕ) => PartialTree ι) ↑i) (ℕ → PartialTree ι)

The Ionescu–Tulcea trajectory kernel of the generation chain.

Equations

• ProbabilityTheory.GaltonWatson.chainTraj ξ n = ProbabilityTheory.Kernel.traj (ProbabilityTheory.GaltonWatson.chainKernel ξ) n

noncomputable def ProbabilityTheory.GaltonWatson.trajectory {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] (s : PartialTree ι) : MeasureTheory.Measure (ℕ → PartialTree ι)

The law of the whole trajectory of generations started at a partial tree.

Equations

• ProbabilityTheory.GaltonWatson.trajectory ξ s = (ProbabilityTheory.GaltonWatson.chainTraj ξ 0) fun (x : ↥(Finset.Iic 0)) => s

instance ProbabilityTheory.GaltonWatson.instIsProbabilityMeasureForallNatPartialTreeTrajectory {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [IsMarkovKernel ξ] (s : PartialTree ι) : MeasureTheory.IsProbabilityMeasure (trajectory ξ s)

theorem ProbabilityTheory.GaltonWatson.trajectory_map_eval {ι : Type u_1} [MeasurableSpace ι] (ξ : Kernel ι (List ι)) [Countable ι] [IsMarkovKernel ξ] (s : PartialTree ι) (n : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → PartialTree ι) => ω n) (trajectory ξ s) = (generation ξ ^ n) s

At time n the generation chain is distributed as n synchronous generations.