Independent groups of potential offspring coordinates

Group zero contains the root coordinate and the unused addresses; group i + 1 contains all addresses below child i + 1. The explicit injection branchAddress retains the coordinates needed for any finite family of child subtrees. Its pushforward under an i.i.d. field is the product of k + 1 independent i.i.d. fields. Adapted from Freezing1/OffspringFieldGroups.lean.

def BGW.LocallyFinite.branchAddress (k : ℕ) (q : Fin (k + 1) × Address) : Address

Regroup the addresses: the pair (i, u) with i ≠ 0 is the address u below child i, while (0, u) is the root coordinate and the addresses u shifted past the first k children (so that it never meets another group).

Equations

• BGW.LocallyFinite.branchAddress k q = if q.1 = 0 then match q.2 with | [] => [] | j :: u => (k + 1 + j) :: u else ↑q.1 :: q.2

theorem BGW.LocallyFinite.branchAddress_injective (k : ℕ) : Function.Injective (branchAddress k)

theorem BGW.LocallyFinite.iid_branch_groups (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.Measure.map (fun (f : Address → ℕ) (i : Fin (k + 1)) (u : Address) => f (branchAddress k (i, u))) (MeasureTheory.Measure.infinitePi fun (x : Address) => μ) = MeasureTheory.Measure.pi fun (x : Fin (k + 1)) => MeasureTheory.Measure.infinitePi fun (x : Address) => μ

Regrouping an i.i.d. field of offspring counts yields independent i.i.d. fields.