Finite offspring cylinders and their root decomposition

After fixing the root offspring count, a finite cylinder splits into the cylinders of the children and deterministic zero constraints at absent addresses. This is the finite-coordinate input to the uniqueness of a branching law. Adapted from Freezing1/PlaneTreeOffspringCylinders.lean.

def BGW.LocallyFinite.offspringCylinder (F : Finset Address) (E : Address → Set ℕ) : Set Tree

The cylinder fixing the offspring coordinates at the finitely many addresses of F.

Equations

• BGW.LocallyFinite.offspringCylinder F E = {T : BGW.LocallyFinite.Tree | ∀ u ∈ F, ↑T u ∈ E u}

theorem BGW.LocallyFinite.measurableSet_offspringCylinder (F : Finset Address) (E : Address → Set ℕ) : MeasurableSet (offspringCylinder F E)

noncomputable def BGW.LocallyFinite.childIndices (F : Finset Address) (j : ℕ) : Finset Address

The addresses of F below the child j, with the leading j removed.

Equations

• BGW.LocallyFinite.childIndices F j = F.preimage (List.cons j) ⋯

@[simp]

theorem BGW.LocallyFinite.mem_childIndices (F : Finset Address) (j : ℕ) (u : Address) : u ∈ childIndices F j ↔ j :: u ∈ F

def BGW.LocallyFinite.rootCompatible (F : Finset Address) (E : Address → Set ℕ) (k : ℕ) : Prop

Compatibility of a root degree k with the root and absent-child constraints of a cylinder: the root coordinate must be allowed, and a coordinate below an invalid child, which is zero, must be allowed too.

Equations

• BGW.LocallyFinite.rootCompatible F E k = ∀ u ∈ F, match u with | [] => k ∈ E [] | j :: v => ¬(1 ≤ j ∧ j ≤ k) → 0 ∈ E (j :: v)

theorem BGW.LocallyFinite.mem_offspringCylinder_iff_root (F : Finset Address) (E : Address → Set ℕ) (T : Tree) (k : ℕ) (hd : degree T = k) : T ∈ offspringCylinder F E ↔ rootCompatible F E k ∧ ∀ (i : Fin k), child T (↑i + 1) ∈ offspringCylinder (childIndices F (↑i + 1)) fun (u : Address) => E ((↑i + 1) :: u)

theorem BGW.LocallyFinite.childIndices_length_le (F : Finset Address) (n j : ℕ) (hF : ∀ u ∈ F, List.length u ≤ n + 1) (u : Address) : u ∈ childIndices F j → List.length u ≤ n