Canonical pruning of an offspring field

An arbitrary field of potential offspring counts, indexed by all addresses, is turned into a canonical tree by keeping the counts at addresses that exist and setting every other coordinate to zero. This is the standard construction of a locally finite tree from i.i.d. offspring counts; it is adapted from Freezing1/PlaneTreePruning.lean.

A retained coordinate equal to zero is a present leaf, whereas the coordinates below an absent address are all discarded: prune_val_of_present and not_present_offspring_zero together describe prune f. The map is the identity on canonical fields (prune_val) and measurable from the product σ-algebra on Offspring to the subtype σ-algebra on Tree, which is its Borel σ-algebra (see BGW/LocallyFinite/Topology.lean).

def BGW.LocallyFinite.pruneRaw (f : Offspring) : Address → ℕ

Keep the offspring count at an address only if every step of the address is a valid child of the retained counts above it.

Equations

• BGW.LocallyFinite.pruneRaw f [] = f []
• BGW.LocallyFinite.pruneRaw f (j :: u) = if 1 ≤ j ∧ j ≤ f [] then BGW.LocallyFinite.pruneRaw (fun (v : BGW.LocallyFinite.Address) => f (j :: v)) u else 0

theorem BGW.LocallyFinite.canonical_pruneRaw (f : Offspring) : Canonical (pruneRaw f)

def BGW.LocallyFinite.prune (f : Offspring) : Tree

The tree obtained from an offspring field by discarding the counts at absent addresses.

Equations

• BGW.LocallyFinite.prune f = ⟨BGW.LocallyFinite.pruneRaw f, ⋯⟩

@[simp]

theorem BGW.LocallyFinite.degree_prune (f : Offspring) : degree (prune f) = f []

theorem BGW.LocallyFinite.child_prune (f : Offspring) (j : ℕ) : child (prune f) j = if 1 ≤ j ∧ j ≤ f [] then prune fun (v : Address) => f (j :: v) else leaf

theorem BGW.LocallyFinite.pruneRaw_eq_of_canonical {f : Offspring} (hf : Canonical f) (u : Address) : pruneRaw f u = f u

@[simp]

theorem BGW.LocallyFinite.prune_val (T : Tree) : prune ↑T = T

Pruning does not change a field that is already canonical.

theorem BGW.LocallyFinite.measurable_pruneRaw_eval (u : Address) : Measurable fun (f : Offspring) => pruneRaw f u

theorem BGW.LocallyFinite.prune_val_of_present {f : Offspring} {u : Address} (h : Present (prune f) u) : ↑(prune f) u = f u

At a present address the pruned tree keeps the original count.

theorem BGW.LocallyFinite.measurable_prune : Measurable prune