Replacing a fringe subtree inside a root occurrence of H_{r,k}

Deterministic part of the proofs of Lemmas lem:S_rary(ii) and lem:C_rary (source lines 2670–2753 and 2768–2792; inventory P19, P21). Let H_{r,k} ≺ T (r ≥ 1) and let u be the vertex of DFS index ℓ of T.

• embeds_completeTree_replaceAt (P21): if k_u(T) ≠ r, then u is not an internal vertex of the displayed copy of H_{r,k}, and replacing T_u by any tree preserves H_{r,k} ≺ T.
• ReplaceClass r k T ℓ j (P19): after replacing T_u by S, H_{r,k} ≺ T[S/T_u] holds iff H_{r,j} ≺ S. exists_replaceClass: every position has such a class j ≤ k — j = 0 when u is a leaf of the displayed skeleton or lies in the grafted forest, j = k - a when u is an internal skeleton vertex at depth a (the paper's "the displayed skeleton already provides a complete r-ary continuation of height k - a").
• classCount_le (P19, the count of skeleton vertices): for j ≥ 1 at most r^{k-j} positions of T are of class j (there are r^a skeleton vertices at depth a).

theorem PoissonDeclumping.PlaneTree.embeds_completeTree_self {r : ℕ} (hr : 1 ≤ r) (a : ℕ) : (completeTree r a).Embeds (completeTree r a)

Embeds (H_{r,a}) (H_{r,a}).

theorem PoissonDeclumping.PlaneTree.le_of_embeds_completeTree {r : ℕ} (hr : 1 ≤ r) {a b : ℕ} : (completeTree r a).Embeds (completeTree r b) → a ≤ b

H_{r,a} ≺ H_{r,b} implies a ≤ b (r ≥ 1).

theorem PoissonDeclumping.PlaneTree.not_embeds_completeTree_leaf {r j : ℕ} (hr : 1 ≤ r) (hj : 1 ≤ j) : ¬(completeTree r j).Embeds (node [])

A leaf supports no H_{r,j} with j ≥ 1 (r ≥ 1).

theorem PoissonDeclumping.PlaneTree.embeds_completeTree_replaceAt {r : ℕ} (k : ℕ) {T : PlaneTree} {ℓ : ℕ} : (completeTree r k).Embeds T → ℓ < T.vertexCount → (T.fringeAt ℓ).rootDegree ≠ r → ∀ (S : PlaneTree), (completeTree r k).Embeds (T.replaceAt ℓ S)

P21. If H_{r,k} ≺ T and the vertex u of DFS index ℓ has k_u(T) ≠ r, then u is not an internal vertex of the displayed copy of H_{r,k}, so arbitrary re-grafting at u preserves H_{r,k} ≺ · (source lines 2775–2783). Valid for every r (for r = 0 the pattern is a single vertex).

def PoissonDeclumping.PlaneTree.ReplaceClass (r k : ℕ) (T : PlaneTree) (ℓ j : ℕ) : Prop

The class j of the DFS position ℓ of T with respect to H_{r,k}: re-grafting any S at the vertex u_{ℓ+1}(T) gives H_{r,k} ≺ T[S/T_{u_{ℓ+1}}] iff H_{r,j} ≺ S.

Equations

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

theorem PoissonDeclumping.PlaneTree.replaceClass_succ_node_append {r k : ℕ} (hr : 1 ≤ r) {pre post : List PlaneTree} {t : PlaneTree} (hT : (completeTree r (k + 1)).Embeds (node (pre ++ t :: post))) {q : ℕ} (hq : q < t.vertexCount) (j : ℕ) : ReplaceClass r (k + 1) (node (pre ++ t :: post)) (forestSize pre + q + 1) j ↔ ReplaceClass r k t q j

The class of a position inside a child: if H_{r,k+1} ≺ node (pre ++ t :: post), the position forestSize pre + q + 1 has class j w.r.t. H_{r,k+1} iff the position q of t has class j w.r.t. H_{r,k}.

theorem PoissonDeclumping.PlaneTree.replaceClass_zero_iff {r k : ℕ} (hr : 1 ≤ r) (T : PlaneTree) (j : ℕ) : ReplaceClass r k T 0 j ↔ j = k

At the root (ℓ = 0) the class is k, and only k.

theorem PoissonDeclumping.PlaneTree.exists_replaceClass {r : ℕ} (hr : 1 ≤ r) (k : ℕ) {T : PlaneTree} {ℓ : ℕ} : (completeTree r k).Embeds T → ℓ < T.vertexCount → ∃ j ≤ k, ReplaceClass r k T ℓ j

Classification (P19). If H_{r,k} ≺ T (r ≥ 1), every DFS position of T has a class j ≤ k.

noncomputable def PoissonDeclumping.PlaneTree.classCount (r k : ℕ) (T : PlaneTree) (j : ℕ) : ENNReal

The number of DFS positions of T of class j (with respect to H_{r,k}).

Equations

• PoissonDeclumping.PlaneTree.classCount r k T j = ∑ ℓ ∈ Finset.range T.vertexCount, {ℓ : ℕ | PoissonDeclumping.PlaneTree.ReplaceClass r k T ℓ j}.indicator 1 ℓ

def PoissonDeclumping.PlaneTree.classBound (r k j : ℕ) : ℕ

The bound r^{k-j} (for j ≤ k, else 0) on the number of positions of class j ≥ 1: the internal skeleton vertices at depth k - j.

Equations

• PoissonDeclumping.PlaneTree.classBound r k j = if j ≤ k then r ^ (k - j) else 0

theorem PoissonDeclumping.PlaneTree.indicator_one_eq_of_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} {b : β} (h : a ∈ s ↔ b ∈ t) : s.indicator 1 a = t.indicator 1 b

theorem PoissonDeclumping.PlaneTree.classCount_le {r : ℕ} (hr : 1 ≤ r) (k : ℕ) {T : PlaneTree} {j : ℕ} : (completeTree r k).Embeds T → 1 ≤ j → classCount r k T j ≤ ↑(classBound r k j)

Count of skeleton positions (P19). If H_{r,k} ≺ T (r ≥ 1) and j ≥ 1, at most r^{k-j} DFS positions of T have class j (none if j > k).