Documentation

BGW.LocallyFinite.Generation

Finite generations of locally finite trees #

generation T n lists exactly the present addresses of length n, with the root at generation zero. Its cardinality is generationSize T n. The definition adapts the finite-generation construction of Freezing1/PlaneTreeGeometry.lean; indices in Finset.range are shifted by one to retain the positive child convention. No finiteness of the whole tree is assumed.

source
def BGW.LocallyFinite.generation (T : Tree) :
ℕ → Finset Address

The finite set of vertices at depth n, including the root at depth zero.

Equations
Instances For
    source
    theorem BGW.LocallyFinite.mem_generation (T : Tree) (n : ℕ) (u : Address) :
    u ∈ generation T n ↔ Present T u ∧ List.length u = n
    source
    def BGW.LocallyFinite.generationSize (T : Tree) (n : ℕ) :
    ℕ

    The number of present vertices at depth n.

    Equations
    Instances For
      source
      @[simp]
      theorem BGW.LocallyFinite.generationSize_zero (T : Tree) :
      generationSize T 0 = 1
      source
      theorem BGW.LocallyFinite.generationSize_succ (T : Tree) (n : ℕ) :
      generationSize T (n + 1) = ∑ j ∈ Finset.range (degree T), generationSize (child T (j + 1)) n

      A generation is the disjoint union of the corresponding generations of existing children.

      source
      theorem BGW.LocallyFinite.generationSize_succ_eq_sum (T : Tree) (n : ℕ) :
      generationSize T (n + 1) = ∑ i : Fin (degree T), generationSize (child T (↑i + 1)) n
      source
      @[simp]
      theorem BGW.LocallyFinite.generationSize_one (T : Tree) :
      generationSize T 1 = degree T
      source
      theorem BGW.LocallyFinite.generationSize_eq_zero_iff (T : Tree) (n : ℕ) :
      generationSize T n = 0 ↔ T ∈ extinctBy n

      No vertex at depth n is equivalent to extinction by generation n.

      source
      theorem BGW.PlaneTree.generation_toLocallyFinite (t : PlaneTree) (n : ℕ) :
      LocallyFinite.generation t.toLocallyFinite n = Finset.image positiveAddress ({u ∈ t.vertices.toFinset | u.length = n})

      The finite-tree bridge shifts child indices and preserves every generation.

      source
      theorem BGW.PlaneTree.generationSize_toLocallyFinite (t : PlaneTree) (n : ℕ) :
      LocallyFinite.generationSize t.toLocallyFinite n = t.generationSize n