Documentation

BGW.StableTrees.DiscreteForestBlocks

Decoding finite ladder blocks #

On paths reaching every negative integer level, consecutive first-passage times cut out finite tree excursions. Their record counts agree with DFS heights. Each block is also viewed as a point of the locally finite tree space.

source
noncomputable def BGW.StableTrees.DiscreteForest.blockDegrees (ω : ℕ → ℕ) (r : ℕ) :
List ℕ

The degree sequence of the r-th block ω_{L r}, ..., ω_{L(r+1)-1}.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def BGW.StableTrees.DiscreteForest.blockTree (ω : ℕ → ℕ) (r : ℕ) :
    PlaneTree

    The r-th block tree, with a leaf fallback when decoding blockDegrees fails.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.DiscreteForest.degrees_blockTree {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) :
      (blockTree ω r).degrees = blockDegrees ω r

      On LadderFinite, the block decodes to a tree with the block's degrees.

      source
      theorem BGW.StableTrees.DiscreteForest.size_blockTree {ω : ℕ → ℕ} (hω : LadderFinite ω) (r : ℕ) :
      (blockTree ω r).size = ladderTime ω (r + 1) - ladderTime ω r

      The size of the r-th block tree is L (r+1) - L r.

      source
      theorem BGW.StableTrees.DiscreteForest.forestHeight_eq_treeHeight {ω : ℕ → ℕ} (hω : LadderFinite ω) (r i : ℕ) (hi : i < (blockTree ω r).size) :
      forestHeight ω (ladderTime ω r + i) = (blockTree ω r).height ⟨i, hi⟩

      The record-count height of the forest equals the tree height on each block.

      source
      noncomputable def BGW.StableTrees.DiscreteForest.blockLF (ω : ℕ → ℕ) (r : ℕ) :
      LocallyFinite.Tree

      The block as a point of the locally finite tree space.

      Equations
      Instances For