Documentation

BGW.LocallyFinite.GenerationProcess

Generation histories and offspring transitions #

The offspring counts on the current generation use coordinates disjoint from those which determine the preceding generations. Splitting by the finite set of current vertices gives the transition law without imposing positive probability on a history.

source
def BGW.LocallyFinite.generationHistory (n : ℕ) (z : Fin (n + 1) → ℕ) :
Set Tree

The prescribed sizes of generations zero through n, including both endpoints.

Equations
Instances For
    source
    theorem BGW.LocallyFinite.measurableSet_generationHistory (n : ℕ) (z : Fin (n + 1) → ℕ) :
    MeasurableSet (generationHistory n z)
    source
    theorem BGW.LocallyFinite.bienaymeLaw_generationHistory_next (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (z : Fin (n + 1) → ℕ) (k : ℕ) :
    (bienaymeLaw μ) (generationHistory n z ∩ {T : Tree | generationSize T (n + 1) = k}) = (bienaymeLaw μ) (generationHistory n z) * (MeasureTheory.Measure.pi fun (x : Fin (z (Fin.last n))) => μ) {v : Fin (z (Fin.last n)) → ℕ | ∑ i : Fin (z (Fin.last n)), v i = k}

    The transition law of generation sizes given their full finite history. This identity of joint masses also applies to histories of probability zero.

    source
    theorem BGW.LocallyFinite.cond_generationHistory_next (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (z : Fin (n + 1) → ℕ) (k : ℕ) (hz : (bienaymeLaw μ) (generationHistory n z) ≠ 0) :
    (bienaymeLaw μ)[{T : Tree | generationSize T (n + 1) = k} | generationHistory n z] = (MeasureTheory.Measure.pi fun (x : Fin (z (Fin.last n))) => μ) {v : Fin (z (Fin.last n)) → ℕ | ∑ i : Fin (z (Fin.last n)), v i = k}

    At a history of positive probability, the next size is a sum of as many iid offspring counts as there are individuals in the current generation.

    source
    theorem BGW.LocallyFinite.generationSize_succ_eq_zero_of_eq_zero {T : Tree} {n : ℕ} (h : generationSize T n = 0) :
    generationSize T (n + 1) = 0

    Extinction is absorbing: an empty generation has no descendants in the next generation.