The Łukasiewicz coding of plane trees

Section 2.1 of the paper (source lines 683–696) and Section 2.3 (source lines 735–736).

• PlaneTree.dfsSeq T is the DFS sequence 𝐱(T) = (k_{u_1}(T) - 1, …, k_{u_n}(T) - 1).
• Its partial sums are nonnegative before time n = |T| and equal -1 at time n, so ζ(𝐱(T) ++ 𝐲) = |T| for every continuation 𝐲 (zeta_dfsSeq_append).
• The coding is injective and even prefix-free (dfsSeq_append_inj), and its range is exactly the set of sequences with increments ≥ -1 whose first passage time to -1 is their length (mem_range_dfsSeq_iff).
• PlaneTree.ofSeq 𝐱 is the paper's T(𝐱): the tree whose DFS sequence is (x_1, …, x_{ζ(𝐱)}).
• eq:fringe: the i-th cyclic shift of 𝐱(T), stopped at its first passage time to -1, is the DFS sequence of the fringe subtree at the i-th vertex (ofSeq_rotate_dfsSeq).

Forests (lists of trees) are coded by concatenation (PlaneTree.forestSeq); a forest of k trees corresponds to a sequence with first passage to -k at its end.

def PoissonDeclumping.PlaneTree.dfsSeq (T : PlaneTree) : List ℤ

The DFS sequence 𝐱(T) = (k_{u_1}(T) - 1, …, k_{u_n}(T) - 1) of a plane tree.

Equations

• T.dfsSeq = List.map (fun (d : ℕ) => ↑d - 1) T.degSeq

def PoissonDeclumping.PlaneTree.forestSeq (ts : List PlaneTree) : List ℤ

The DFS sequence of a forest: the concatenation of the DFS sequences of its trees.

Equations

• PoissonDeclumping.PlaneTree.forestSeq ts = List.flatMap PoissonDeclumping.PlaneTree.dfsSeq ts

@[simp]

theorem PoissonDeclumping.PlaneTree.forestSeq_nil : forestSeq [] = []

@[simp]

theorem PoissonDeclumping.PlaneTree.forestSeq_cons (t : PlaneTree) (ts : List PlaneTree) : forestSeq (t :: ts) = t.dfsSeq ++ forestSeq ts

theorem PoissonDeclumping.PlaneTree.forestSeq_append (ts us : List PlaneTree) : forestSeq (ts ++ us) = forestSeq ts ++ forestSeq us

theorem PoissonDeclumping.PlaneTree.dfsSeq_node (ts : List PlaneTree) : (node ts).dfsSeq = (↑ts.length - 1) :: forestSeq ts

theorem PoissonDeclumping.PlaneTree.length_dfsSeq (T : PlaneTree) : T.dfsSeq.length = T.vertexCount

theorem PoissonDeclumping.PlaneTree.one_le_vertexCount (T : PlaneTree) : 1 ≤ T.vertexCount

theorem PoissonDeclumping.PlaneTree.neg_one_le_of_mem_dfsSeq {T : PlaneTree} {a : ℤ} (ha : a ∈ T.dfsSeq) : -1 ≤ a

Every entry of a DFS sequence is at least -1.

theorem PoissonDeclumping.PlaneTree.forestSeq_excursion {ts : List PlaneTree} (h : ∀ t ∈ ts, t.dfsSeq.sum = -1 ∧ ∀ j < t.dfsSeq.length, 0 ≤ (List.take j t.dfsSeq).sum) : (forestSeq ts).sum = -↑ts.length ∧ ∀ j < (forestSeq ts).length, -↑ts.length < (List.take j (forestSeq ts)).sum

Excursion property of forests, given the excursion property of every tree.

theorem PoissonDeclumping.PlaneTree.dfsSeq_excursion (T : PlaneTree) : T.dfsSeq.sum = -1 ∧ ∀ j < T.dfsSeq.length, 0 ≤ (List.take j T.dfsSeq).sum

Łukasiewicz excursion property. The DFS sequence of a tree sums to -1, and all its proper partial sums are nonnegative.

theorem PoissonDeclumping.PlaneTree.sum_dfsSeq (T : PlaneTree) : T.dfsSeq.sum = -1

theorem PoissonDeclumping.PlaneTree.sum_take_dfsSeq_nonneg (T : PlaneTree) {j : ℕ} (hj : j < T.vertexCount) : 0 ≤ (List.take j T.dfsSeq).sum

All proper partial sums of a DFS sequence are nonnegative (before ζ).

theorem PoissonDeclumping.PlaneTree.sum_forestSeq (ts : List PlaneTree) : (forestSeq ts).sum = -↑ts.length

theorem PoissonDeclumping.PlaneTree.zeta_dfsSeq_append (T : PlaneTree) (y : List ℤ) : Lukasiewicz.zeta (T.dfsSeq ++ y) = some T.vertexCount

Łukasiewicz coding (B02). For every tree T and every continuation 𝐲, ζ(𝐱(T) 𝐲) = |T|.

theorem PoissonDeclumping.PlaneTree.zeta_dfsSeq (T : PlaneTree) : Lukasiewicz.zeta T.dfsSeq = some T.vertexCount

theorem PoissonDeclumping.PlaneTree.dfsSeq_append_inj {T U : PlaneTree} {y z : List ℤ} (h : T.dfsSeq ++ y = U.dfsSeq ++ z) : T = U ∧ y = z

The coding is prefix-free: a DFS sequence determines its tree even when followed by an arbitrary continuation.

theorem PoissonDeclumping.PlaneTree.dfsSeq_injective : Function.Injective dfsSeq

The DFS sequence determines the tree.

theorem PoissonDeclumping.PlaneTree.degSeq_injective : Function.Injective degSeq

The outdegree sequence in DFS order determines the tree.

theorem PoissonDeclumping.PlaneTree.exists_forestSeq_eq (x : List ℤ) (hx : ∀ a ∈ x, -1 ≤ a) (k : ℕ) (hs : x.sum = -↑k) (hp : ∀ j < x.length, -↑k < (List.take j x).sum) : ∃ (ts : List PlaneTree), ts.length = k ∧ forestSeq ts = x

Every sequence with increments ≥ -1 and first passage to -k exactly at its end is the DFS sequence of a forest of k trees.

theorem PoissonDeclumping.PlaneTree.exists_dfsSeq_eq_take {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {m : ℕ} (hz : Lukasiewicz.zeta x = some m) : ∃ (T : PlaneTree), T.dfsSeq = List.take m x ∧ T.vertexCount = m

Łukasiewicz coding, surjectivity (B02). If 𝐱 has increments ≥ -1 and ζ(𝐱) = m < ∞, then (x_1, …, x_m) is the DFS sequence of a tree (with m vertices).

noncomputable def PoissonDeclumping.PlaneTree.ofSeq (x : List ℤ) : Option PlaneTree

The paper's T(𝐱): the tree whose DFS sequence is (x_1, …, x_{ζ(𝐱)}), if ζ(𝐱) < ∞ and this prefix is a DFS sequence (which holds whenever all increments are ≥ -1), and none otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem PoissonDeclumping.PlaneTree.ofSeq_eq_some_iff {x : List ℤ} {T : PlaneTree} : ofSeq x = some T ↔ ∃ (m : ℕ), Lukasiewicz.zeta x = some m ∧ T.dfsSeq = List.take m x

Characterization of T(𝐱).

theorem PoissonDeclumping.PlaneTree.ofSeq_dfsSeq_append (T : PlaneTree) (y : List ℤ) : ofSeq (T.dfsSeq ++ y) = some T

T(𝐱(T) 𝐲) = T for every continuation 𝐲.

theorem PoissonDeclumping.PlaneTree.ofSeq_dfsSeq (T : PlaneTree) : ofSeq T.dfsSeq = some T

theorem PoissonDeclumping.PlaneTree.exists_ofSeq_eq_some {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) {m : ℕ} (hz : Lukasiewicz.zeta x = some m) : ∃ (T : PlaneTree), ofSeq x = some T ∧ T.dfsSeq = List.take m x ∧ T.vertexCount = m

If 𝐱 has increments ≥ -1 and ζ(𝐱) = m < ∞, then T(𝐱) is defined, has m vertices, and its DFS sequence is (x_1, …, x_m).

theorem PoissonDeclumping.PlaneTree.isSome_ofSeq_iff {x : List ℤ} (hx : ∀ a ∈ x, -1 ≤ a) : (ofSeq x).isSome = true ↔ (Lukasiewicz.zeta x).isSome = true

For sequences with increments ≥ -1, T(𝐱) is defined exactly when ζ(𝐱) < ∞.

theorem PoissonDeclumping.PlaneTree.mem_range_dfsSeq_iff {x : List ℤ} : x ∈ Set.range dfsSeq ↔ (∀ a ∈ x, -1 ≤ a) ∧ Lukasiewicz.zeta x = some x.length

The range of the coding: a finite sequence is a DFS sequence iff its increments are ≥ -1 and its first passage time to -1 is its length.

Fringe subtrees and cyclic shifts (eq:fringe)

theorem PoissonDeclumping.PlaneTree.dfsSeq_fringeTrees_prefix (T : PlaneTree) (i : ℕ) (hi : i < T.fringeTrees.length) : T.fringeTrees[i].dfsSeq <+: List.drop i T.dfsSeq

The DFS sequence of the fringe subtree at the i-th vertex (in DFS order, 0-indexed) is a contiguous block of 𝐱(T) starting at position i.

theorem PoissonDeclumping.PlaneTree.lt_length_fringeTrees {T : PlaneTree} {i : ℕ} (hi : i < T.vertexCount) : i < T.fringeTrees.length

Index bound transfer: |T| is the length of the list of fringe trees.

theorem PoissonDeclumping.PlaneTree.exists_rotate_dfsSeq_eq (T : PlaneTree) (i : ℕ) (hi : i < T.vertexCount) : ∃ (y : List ℤ), T.dfsSeq.rotate i = T.fringeTrees[i].dfsSeq ++ y

The i-th cyclic shift of 𝐱(T) starts with the DFS sequence of the fringe subtree at the i-th vertex.

theorem PoissonDeclumping.PlaneTree.zeta_rotate_dfsSeq (T : PlaneTree) (i : ℕ) (hi : i < T.vertexCount) : Lukasiewicz.zeta (T.dfsSeq.rotate i) = some T.fringeTrees[i].vertexCount

eq:fringe. The i-th cyclic shift of 𝐱(T) first hits -1 at the size of the fringe subtree T_{u_i} at the i-th vertex.

theorem PoissonDeclumping.PlaneTree.take_rotate_dfsSeq (T : PlaneTree) (i : ℕ) (hi : i < T.vertexCount) : List.take T.fringeTrees[i].vertexCount (T.dfsSeq.rotate i) = T.fringeTrees[i].dfsSeq

eq:fringe. The i-th cyclic shift of 𝐱(T), up to its first passage time to -1, is the DFS sequence of the fringe subtree T_{u_i}.

theorem PoissonDeclumping.PlaneTree.ofSeq_rotate_dfsSeq (T : PlaneTree) (i : ℕ) (hi : i < T.vertexCount) : ofSeq (T.dfsSeq.rotate i) = some T.fringeTrees[i]

eq:fringe. T(𝐱^{(i)}(T)) = T_{u_i}.