Generations determined by an offspring field

The generations through depth n only depend on offspring coordinates strictly above depth n. The next generation is the sum of the offspring counts at the current generation. These deterministic facts separate the explored field from fresh offspring coordinates in the generation-process law.

def BGW.LocallyFinite.cutField (n : ℕ) (f : Offspring) : Offspring

Retain offspring coordinates strictly above depth n and set all others to zero.

Equations

• BGW.LocallyFinite.cutField n f u = if List.length u < n then f u else 0

theorem BGW.LocallyFinite.measurable_cutField (n : ℕ) : Measurable (cutField n)

theorem BGW.LocallyFinite.generation_prune_cutField (n m : ℕ) (hm : m ≤ n) (f : Offspring) : generation (prune (cutField n f)) m = generation (prune f) m

Offspring counts at depth n and below do not affect any generation through depth n.

theorem BGW.LocallyFinite.generationSize_succ_eq_sum_offspring (T : Tree) (n : ℕ) : generationSize T (n + 1) = ∑ u ∈ generation T n, ↑T u

The next generation counts all children of vertices in the current generation.

theorem BGW.LocallyFinite.generationSize_prune_succ (f : Offspring) (n : ℕ) : generationSize (prune f) (n + 1) = ∑ u ∈ generation (prune f) n, f u

At present vertices pruning keeps the original offspring counts.

theorem BGW.LocallyFinite.measurableSet_present (u : Address) : MeasurableSet {T : Tree | Present T u}

theorem BGW.LocallyFinite.measurable_generation (n : ℕ) : Measurable fun (T : Tree) => generation T n

theorem BGW.LocallyFinite.measurableSet_generation_eq (n : ℕ) (S : Finset Address) : MeasurableSet {T : Tree | generation T n = S}