Generations of a plane tree

A minimal generation API for the proof of Lemma lem:S_lh (source lines 3066–3083, inventory P23):

• gen i T: the fringe subtrees rooted at the vertices of generation (depth) i, in depth-first order (one entry per vertex, multiplicity preserved);
• genCount i T = Z_i(T): the number of vertices at generation i;
• skelSize k T = C_k(T) = Z_0(T) + ⋯ + Z_{k-1}(T): the number of vertices in the first k generations (the paper's skeleton size), while L_k(T) = Z_k(T) = (gen k T).length;
• vertexCount_eq_skelSize_add: |T| = C_k(T) + ∑_{v ∈ gen k T} |T_v|, the deterministic identity behind the decomposition |𝒯| = C_k + ∑_{i ≤ L_k} |𝒯^{(i)}|.

def PoissonDeclumping.PlaneTree.gen : ℕ → PlaneTree → List PlaneTree

The fringe subtrees rooted at generation i, in depth-first order.

Equations

• PoissonDeclumping.PlaneTree.gen 0 x✝ = [x✝]
• PoissonDeclumping.PlaneTree.gen i.succ x✝ = List.flatMap (PoissonDeclumping.PlaneTree.gen i) x✝.children

def PoissonDeclumping.PlaneTree.genCount (i : ℕ) (T : PlaneTree) : ℕ

Z_i(T), the number of vertices of T at generation i.

Equations

• PoissonDeclumping.PlaneTree.genCount i T = (PoissonDeclumping.PlaneTree.gen i T).length

def PoissonDeclumping.PlaneTree.skelSize (k : ℕ) (T : PlaneTree) : ℕ

C_k(T) = ∑_{i < k} Z_i(T), the number of vertices in generations 0, …, k - 1.

Equations

• PoissonDeclumping.PlaneTree.skelSize k T = ∑ i ∈ Finset.range k, PoissonDeclumping.PlaneTree.genCount i T

@[simp]

theorem PoissonDeclumping.PlaneTree.gen_zero (T : PlaneTree) : gen 0 T = [T]

theorem PoissonDeclumping.PlaneTree.gen_succ (i : ℕ) (T : PlaneTree) : gen (i + 1) T = List.flatMap (gen i) T.children

@[simp]

theorem PoissonDeclumping.PlaneTree.gen_succ_node (i : ℕ) (ts : List PlaneTree) : gen (i + 1) (node ts) = List.flatMap (gen i) ts

@[simp]

theorem PoissonDeclumping.PlaneTree.genCount_zero (T : PlaneTree) : genCount 0 T = 1

theorem PoissonDeclumping.PlaneTree.genCount_succ (i : ℕ) (T : PlaneTree) : genCount (i + 1) T = (List.map (genCount i) T.children).sum

theorem PoissonDeclumping.PlaneTree.genCount_succ_node (i : ℕ) (ts : List PlaneTree) : genCount (i + 1) (node ts) = (List.map (genCount i) ts).sum

@[simp]

theorem PoissonDeclumping.PlaneTree.skelSize_zero (T : PlaneTree) : skelSize 0 T = 0

theorem PoissonDeclumping.PlaneTree.skelSize_succ (k : ℕ) (T : PlaneTree) : skelSize (k + 1) T = (List.map (skelSize k) T.children).sum + 1

C_{k+1}(T) = 1 + ∑_{u ∈ Γ_∅(T)} C_k(T_u).

theorem PoissonDeclumping.PlaneTree.vertexCount_eq_skelSize_add (k : ℕ) (T : PlaneTree) : T.vertexCount = skelSize k T + (List.map vertexCount (gen k T)).sum

|T| = C_k(T) + ∑_{v ∈ gen k T} |T_v| (source lines 3076–3082).