Tree surgery at a non-root DFS position

Combinatorial helpers for the proofs of Lemmas lem:S_rary(ii), lem:C_rary and lem:C_lh (source lines 2670–2753, 2768–2792, 3190–3236; inventory P19, P21, P25), in which a fringe subtree T_{u_{ℓ+1}} at a non-root DFS position ℓ ≥ 1 is cut out and replaced.

A non-root DFS position of node ts lies in exactly one child: writing ts = pre ++ t :: post, the positions of the vertices of t are forestSize pre + q + 1 with q < |t|, where forestSize pre is the total size of the preceding children (the DFS bookkeeping of the paper).

• exists_append_of_lt_forestSize: every position i < forestSize ts of the forest ts is of the form forestSize pre + q with ts = pre ++ t :: post, q < |t|;
• fringeAt_node_append: at that position the fringe subtree of node ts is fringeAt t q;
• replaceAt_node_append: replacing it by S replaces the child t by replaceAt t q S;
• sum_range_forestSize: a sum over the positions of a forest splits over its trees;
• graft_cut_eq_replaceAt: Cut_ℓ(T)[S] is T with T_{u_{ℓ+1}} replaced by S.

def PoissonDeclumping.PlaneTree.forestSize (ts : List PlaneTree) : ℕ

The total number of vertices ∑_i |t_i| of a forest (t_1, …, t_m).

Equations

• PoissonDeclumping.PlaneTree.forestSize ts = (List.map PoissonDeclumping.PlaneTree.vertexCount ts).sum

@[simp]

theorem PoissonDeclumping.PlaneTree.forestSize_nil : forestSize [] = 0

@[simp]

theorem PoissonDeclumping.PlaneTree.forestSize_cons (t : PlaneTree) (ts : List PlaneTree) : forestSize (t :: ts) = t.vertexCount + forestSize ts

theorem PoissonDeclumping.PlaneTree.forestSize_append (ts us : List PlaneTree) : forestSize (ts ++ us) = forestSize ts + forestSize us

theorem PoissonDeclumping.PlaneTree.vertexCount_node_eq (ts : List PlaneTree) : (node ts).vertexCount = forestSize ts + 1

theorem PoissonDeclumping.PlaneTree.length_flatMap_fringeTrees (ts : List PlaneTree) : (List.flatMap fringeTrees ts).length = forestSize ts

theorem PoissonDeclumping.PlaneTree.length_forestSeq (ts : List PlaneTree) : (forestSeq ts).length = forestSize ts

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

theorem PoissonDeclumping.PlaneTree.add_vertexCount_fringeAt_le {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) : i + (T.fringeAt i).vertexCount ≤ T.vertexCount

The fringe subtree at DFS index i fits inside T: i + |T_{u_{i+1}}| ≤ |T|.

theorem PoissonDeclumping.PlaneTree.exists_append_of_lt_forestSize (ts : List PlaneTree) (i : ℕ) : i < forestSize ts → ∃ (pre : List PlaneTree) (t : PlaneTree) (post : List PlaneTree) (q : ℕ), ts = pre ++ t :: post ∧ q < t.vertexCount ∧ i = forestSize pre + q

Every position of a forest lies in exactly one of its trees.

theorem PoissonDeclumping.PlaneTree.fringeAt_node_append (pre post : List PlaneTree) (t : PlaneTree) {q : ℕ} (hq : q < t.vertexCount) : (node (pre ++ t :: post)).fringeAt (forestSize pre + q + 1) = t.fringeAt q

At the DFS position forestSize pre + q + 1 of node (pre ++ t :: post) sits the vertex of DFS index q of the child t.

theorem PoissonDeclumping.PlaneTree.replaceAt_node_append (pre post : List PlaneTree) (t : PlaneTree) {q : ℕ} (hq : q < t.vertexCount) (S : PlaneTree) : (node (pre ++ t :: post)).replaceAt (forestSize pre + q + 1) S = node (pre ++ t.replaceAt q S :: post)

Replacing the fringe subtree at the DFS position forestSize pre + q + 1 of node (pre ++ t :: post) replaces the child t by replaceAt t q S.

theorem PoissonDeclumping.PlaneTree.sum_range_forestSize {M : Type u_1} [AddCommMonoid M] (ts : List PlaneTree) (f : ℕ → M) (g : PlaneTree → ℕ → M) : (∀ (pre : List PlaneTree) (t : PlaneTree) (post : List PlaneTree) (q : ℕ), ts = pre ++ t :: post → q < t.vertexCount → f (forestSize pre + q) = g t q) → ∑ q ∈ Finset.range (forestSize ts), f q = (List.map (fun (t : PlaneTree) => ∑ q ∈ Finset.range t.vertexCount, g t q) ts).sum

A sum over the positions 0 ≤ i < forestSize ts of a forest splits into the sums over the positions of its trees.

theorem PoissonDeclumping.PlaneTree.declumpedMark_replaceAt {B : Set ℕ} {G : PlaneTree → Prop} {T : PlaneTree} {ℓ : ℕ} (S : PlaneTree) (hT : declumpedMark B G T) (hℓ : 1 ≤ ℓ) (hℓT : ℓ < T.vertexCount) (hG : ∀ (t : PlaneTree) (q : ℕ), G t → q < t.vertexCount → t.fringeAt q = T.fringeAt ℓ → G (t.replaceAt q S)) : declumpedMark B G (T.replaceAt ℓ S)

Replacement below the root preserves a declumped mark Ghat = 1{k_∅ ∈ B} 1{∃ child c, G(T_c)} as soon as replacement inside the witnessing child preserves G: the root degree is unchanged, and a witnessing child either does not contain the replaced vertex or is modified only inside. (This is the common step of the proofs of Lemmas lem:C_rary and lem:C_lh.)

theorem PoissonDeclumping.PlaneTree.graft_cut_eq_replaceAt {ℓ : ℕ} {T : PlaneTree} (h : ℓ < T.vertexCount) (S : PlaneTree) : (cut ℓ T).graft S = T.replaceAt ℓ S

Cut_ℓ(T)[S] is the tree T with its fringe subtree T_{u_{ℓ+1}} replaced by S.