Cutting and grafting at a DFS position

Source lines 2487–2509 (Section 6.1 of the paper; inventory U08) and the weight computations in the proof of Lemma lem:cut_graft, lines 2557–2580 (inventory P18).

For a finite plane tree T with |T| ≥ ℓ + 1, the paper's Cut_ℓ(T) replaces the fringe subtree T_{u_{ℓ+1}(T)} at the (ℓ+1)-st vertex in depth-first order by a single marked leaf ⋆; conversely A[S] grafts a tree S at the marked leaf of a marked tree A.

• PlaneTree.fringeAt T i is the fringe subtree at the vertex of DFS index i (0-indexed), so T_{u_{ℓ+1}(T)} = fringeAt T ℓ = T.fringeTrees[ℓ].
• PlaneTree.replaceAt T i S replaces that fringe subtree by S. It is defined through the Łukasiewicz coding: its DFS sequence is the DFS sequence of T with the block of T_{u_{i+1}} replaced by the DFS sequence of S (dfsSeq_replaceAt).
• A PlaneTree.MarkedTree is a plane tree together with the DFS position pos of a marked leaf ⋆. MarkedTree.graft A S = A[S], PlaneTree.cut ℓ T = Cut_ℓ(T), and PlaneTree.cutFamily ℓ = 𝒜_ℓ = {Cut_ℓ(T) : |T| ≥ ℓ + 1}.

Main facts (U08): cut_graft (Cut_ℓ(A[S]) = A), fringeAt_graft (the (ℓ+1)-st fringe subtree of A[S] is S), graft_cut (T = Cut_ℓ(T)[T_{u_{ℓ+1}}]), graft_inj (uniqueness of the decomposition once the position of the marked leaf is fixed), cutFamily_eq (𝒜_ℓ = the marked trees whose marked leaf is the (ℓ+1)-st vertex: the DFS position of ⋆ is preserved), and the bijection cutEquiv.

Weights (P18): MarkedTree.weight μ A = ∏_{v ∈ A, v ≠ ⋆} μ_{k_v(A)} and the exact factorization weight_graft: 𝐏_μ(A[S]) = w(A) 𝐏_μ(S); the sum over cut trees bienayme_cut_mem: 𝐏(|𝒯| ≥ ℓ+1, Cut_ℓ(𝒯) ∈ 𝓡, 𝒯_{u_{ℓ+1}} ∈ F(Cut_ℓ(𝒯))) = ∑_{A ∈ 𝓡} w(A) 𝐏(𝒯 ∈ F(A)). These hold for every offspring law μ (no criticality is used).

Fringe subtree at a DFS position

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

The fringe subtree T_{u_{i+1}(T)} at the vertex of DFS index i (0-indexed). It is T.fringeTrees[i] when i < |T|; for i ≥ |T| it is a (never used) leaf.

Equations

• T.fringeAt i = T.fringeTrees.getD i (PoissonDeclumping.PlaneTree.node [])

theorem PoissonDeclumping.PlaneTree.fringeAt_eq_getElem {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) : T.fringeAt i = T.fringeTrees[i]

theorem PoissonDeclumping.PlaneTree.getElem?_fringeTrees_eq {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) : T.fringeTrees[i]? = some (T.fringeAt i)

theorem PoissonDeclumping.PlaneTree.fringeAt_zero (T : PlaneTree) : T.fringeAt 0 = T

@[simp]

theorem PoissonDeclumping.PlaneTree.vertexCount_leaf : (node []).vertexCount = 1

theorem PoissonDeclumping.PlaneTree.dfsSeq_eq_append_fringeAt (T : PlaneTree) {i : ℕ} (h : i < T.vertexCount) : T.dfsSeq = List.take i T.dfsSeq ++ (T.fringeAt i).dfsSeq ++ List.drop (i + (T.fringeAt i).vertexCount) T.dfsSeq

The DFS sequence of T splits around the block of the fringe subtree at DFS index i.

Splicing DFS sequences

theorem PoissonDeclumping.PlaneTree.exists_dfsSeq_eq_of_excursion {y : List ℤ} (hy : ∀ a ∈ y, -1 ≤ a) (hs : y.sum = -1) (hp : ∀ j < y.length, 0 ≤ (List.take j y).sum) : ∃ (T : PlaneTree), T.dfsSeq = y

A sequence with increments ≥ -1, total sum -1 and nonnegative proper partial sums is a DFS sequence.

theorem PoissonDeclumping.PlaneTree.sum_take_append₃ (a m z : List ℤ) (j : ℕ) : (List.take j (a ++ m ++ z)).sum = (List.take j a).sum + (List.take (j - a.length) m).sum + (List.take (j - a.length - m.length) z).sum

theorem PoissonDeclumping.PlaneTree.exists_dfsSeq_splice {a u z s : List ℤ} (hx : ∃ (T : PlaneTree), T.dfsSeq = a ++ u ++ z) (hu : ∃ (U : PlaneTree), U.dfsSeq = u) (hs : ∃ (S : PlaneTree), S.dfsSeq = s) : ∃ (T₀ : PlaneTree), T₀.dfsSeq = a ++ s ++ z

Replacing a sub-excursion u of a DFS sequence a ++ u ++ z by another DFS sequence s yields a DFS sequence.

Replacing a fringe subtree

noncomputable def PoissonDeclumping.PlaneTree.replaceAt (T : PlaneTree) (i : ℕ) (S : PlaneTree) : PlaneTree

replaceAt T i S: the tree obtained from T by replacing the fringe subtree T_{u_{i+1}(T)} at the vertex of DFS index i by S. It is the tree whose DFS sequence is 𝐱(T) with the block of T_{u_{i+1}} replaced by 𝐱(S) (dfsSeq_replaceAt, for i < |T|).

Equations

• T.replaceAt i S = (PoissonDeclumping.PlaneTree.ofSeq (List.take i T.dfsSeq ++ S.dfsSeq ++ List.drop (i + (T.fringeAt i).vertexCount) T.dfsSeq)).getD T

theorem PoissonDeclumping.PlaneTree.dfsSeq_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : (T.replaceAt i S).dfsSeq = List.take i T.dfsSeq ++ S.dfsSeq ++ List.drop (i + (T.fringeAt i).vertexCount) T.dfsSeq

theorem PoissonDeclumping.PlaneTree.length_take_dfsSeq {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) : (List.take i T.dfsSeq).length = i

theorem PoissonDeclumping.PlaneTree.vertexCount_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : (T.replaceAt i S).vertexCount + (T.fringeAt i).vertexCount = T.vertexCount + S.vertexCount

theorem PoissonDeclumping.PlaneTree.lt_vertexCount_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : i < (T.replaceAt i S).vertexCount

theorem PoissonDeclumping.PlaneTree.take_dfsSeq_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : List.take i (T.replaceAt i S).dfsSeq = List.take i T.dfsSeq

The DFS sequence before position i is unchanged: in particular the vertex where S is grafted keeps its DFS position i.

theorem PoissonDeclumping.PlaneTree.drop_dfsSeq_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : List.drop (i + S.vertexCount) (T.replaceAt i S).dfsSeq = List.drop (i + (T.fringeAt i).vertexCount) T.dfsSeq

theorem PoissonDeclumping.PlaneTree.fringeAt_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : (T.replaceAt i S).fringeAt i = S

After replacement, the fringe subtree at DFS index i is S.

theorem PoissonDeclumping.PlaneTree.replaceAt_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S S' : PlaneTree) : (T.replaceAt i S).replaceAt i S' = T.replaceAt i S'

theorem PoissonDeclumping.PlaneTree.replaceAt_fringeAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) : T.replaceAt i (T.fringeAt i) = T

theorem PoissonDeclumping.PlaneTree.replaceAt_zero (T S : PlaneTree) : T.replaceAt 0 S = S

Replacing at the root (DFS index 0) replaces the whole tree.

theorem PoissonDeclumping.PlaneTree.degSeq_eq_map_dfsSeq (T : PlaneTree) : T.degSeq = List.map (fun (a : ℤ) => (a + 1).toNat) T.dfsSeq

theorem PoissonDeclumping.PlaneTree.degSeq_replaceAt {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (S : PlaneTree) : (T.replaceAt i S).degSeq = List.take i T.degSeq ++ S.degSeq ++ List.drop (i + (T.fringeAt i).vertexCount) T.degSeq

theorem PoissonDeclumping.PlaneTree.degSeq_eq_append_fringeAt (T : PlaneTree) {i : ℕ} (h : i < T.vertexCount) : T.degSeq = List.take i T.degSeq ++ (T.fringeAt i).degSeq ++ List.drop (i + (T.fringeAt i).vertexCount) T.degSeq

theorem PoissonDeclumping.PlaneTree.weight_replaceAt_mul {T : PlaneTree} {i : ℕ} (h : i < T.vertexCount) (μ : PMF ℕ) (S : PlaneTree) : weight μ (T.replaceAt i S) * weight μ (T.fringeAt i) = weight μ T * weight μ S

Bienaymé weights under replacement: 𝐏_μ(T[S/T_{u_{i+1}}]) 𝐏_μ(T_{u_{i+1}}) = 𝐏_μ(T) 𝐏_μ(S).

Marked trees, cut and graft

structure PoissonDeclumping.PlaneTree.MarkedTree : Type

A marked tree: a finite plane tree tree with a marked leaf ⋆, recorded by its DFS index pos (0-indexed, so ⋆ = u_{pos+1}).

• tree : PlaneTree

  The underlying plane tree, in which ⋆ is an ordinary leaf.

• pos : ℕ

  The DFS index of the marked leaf ⋆.

• pos_lt : self.pos < self.tree.vertexCount
• fringeAt_pos : self.tree.fringeAt self.pos = node []

theorem PoissonDeclumping.PlaneTree.MarkedTree.ext {x y : MarkedTree} (tree : x.tree = y.tree) (pos : x.pos = y.pos) : x = y

theorem PoissonDeclumping.PlaneTree.MarkedTree.ext_iff {x y : MarkedTree} : x = y ↔ x.tree = y.tree ∧ x.pos = y.pos

noncomputable def PoissonDeclumping.PlaneTree.MarkedTree.graft (A : MarkedTree) (S : PlaneTree) : PlaneTree

A[S]: graft the tree S at the marked leaf of A.

Equations

• A.graft S = A.tree.replaceAt A.pos S

noncomputable def PoissonDeclumping.PlaneTree.MarkedTree.weight (μ : PMF ℕ) (A : MarkedTree) : ENNReal

w(A) = ∏_{v ∈ A, v ≠ ⋆} μ_{k_v(A)} (source line 2560): the Bienaymé weight of A without the factor of the marked leaf.

Equations

• PoissonDeclumping.PlaneTree.MarkedTree.weight μ A = (List.map (⇑μ) (A.tree.degSeq.eraseIdx A.pos)).prod

theorem PoissonDeclumping.PlaneTree.MarkedTree.pos_lt_vertexCount_graft (A : MarkedTree) (S : PlaneTree) : A.pos < (A.graft S).vertexCount

theorem PoissonDeclumping.PlaneTree.MarkedTree.fringeAt_graft (A : MarkedTree) (S : PlaneTree) : (A.graft S).fringeAt A.pos = S

The fringe subtree of A[S] at the DFS position of ⋆ is S.

theorem PoissonDeclumping.PlaneTree.MarkedTree.vertexCount_graft (A : MarkedTree) (S : PlaneTree) : (A.graft S).vertexCount + 1 = A.tree.vertexCount + S.vertexCount

theorem PoissonDeclumping.PlaneTree.MarkedTree.graft_leaf (A : MarkedTree) : A.graft (node []) = A.tree

theorem PoissonDeclumping.PlaneTree.MarkedTree.degSeq_graft (A : MarkedTree) (S : PlaneTree) : (A.graft S).degSeq = List.take A.pos A.tree.degSeq ++ S.degSeq ++ List.drop (A.pos + 1) A.tree.degSeq

theorem PoissonDeclumping.PlaneTree.MarkedTree.weight_graft (μ : PMF ℕ) (A : MarkedTree) (S : PlaneTree) : PlaneTree.weight μ (A.graft S) = weight μ A * PlaneTree.weight μ S

Weight factorization (source line 2562, inventory P18): 𝐏_μ(𝒯 = A[S]) = w(A) 𝐏_μ(𝒯 = S).

theorem PoissonDeclumping.PlaneTree.MarkedTree.bienayme_singleton_graft (μ : PMF ℕ) (A : MarkedTree) (S : PlaneTree) : (bienayme μ) {A.graft S} = weight μ A * (bienayme μ) {S}

𝐏_μ(𝒯 = A[S]) = w(A) 𝐏_μ(𝒯 = S), as point masses of the Bienaymé measure.

theorem PoissonDeclumping.PlaneTree.MarkedTree.weight_tree (μ : PMF ℕ) (A : MarkedTree) : PlaneTree.weight μ A.tree = weight μ A * μ 0

Consistency check: as an ordinary plane tree, A has weight w(A) μ_0.

noncomputable def PoissonDeclumping.PlaneTree.cut (ℓ : ℕ) (T : PlaneTree) : MarkedTree

Cut_ℓ(T): replace the fringe subtree T_{u_{ℓ+1}(T)} by a marked leaf ⋆, which is then the vertex of DFS index ℓ. Only used for |T| ≥ ℓ + 1 (otherwise a fixed junk value).

Equations

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

theorem PoissonDeclumping.PlaneTree.cut_tree {ℓ : ℕ} {T : PlaneTree} (h : ℓ < T.vertexCount) : (cut ℓ T).tree = T.replaceAt ℓ (node [])

theorem PoissonDeclumping.PlaneTree.cut_pos {ℓ : ℕ} {T : PlaneTree} (h : ℓ < T.vertexCount) : (cut ℓ T).pos = ℓ

The marked leaf of Cut_ℓ(T) is its (ℓ+1)-st vertex: the DFS position is preserved.

theorem PoissonDeclumping.PlaneTree.graft_cut {ℓ : ℕ} {T : PlaneTree} (h : ℓ < T.vertexCount) : (cut ℓ T).graft (T.fringeAt ℓ) = T

T = Cut_ℓ(T)[T_{u_{ℓ+1}(T)}].

theorem PoissonDeclumping.PlaneTree.cut_graft (A : MarkedTree) (S : PlaneTree) : cut A.pos (A.graft S) = A

Cut_ℓ(A[S]) = A when the marked leaf of A is its (ℓ+1)-st vertex.

theorem PoissonDeclumping.PlaneTree.graft_inj {A A' : MarkedTree} {S S' : PlaneTree} (hpos : A.pos = A'.pos) (h : A.graft S = A'.graft S') : A = A' ∧ S = S'

Uniqueness of the decomposition T = A[S] once the position of the marked leaf is fixed.

def PoissonDeclumping.PlaneTree.cutFamily (ℓ : ℕ) : Set MarkedTree

𝒜_ℓ = {Cut_ℓ(T) : |T| ≥ ℓ + 1} (source line 2504).

Equations

• PoissonDeclumping.PlaneTree.cutFamily ℓ = {A : PoissonDeclumping.PlaneTree.MarkedTree | ∃ (T : PoissonDeclumping.PlaneTree), ℓ + 1 ≤ T.vertexCount ∧ PoissonDeclumping.PlaneTree.cut ℓ T = A}

theorem PoissonDeclumping.PlaneTree.cutFamily_eq (ℓ : ℕ) : cutFamily ℓ = {A : MarkedTree | A.pos = ℓ}

𝒜_ℓ consists exactly of the marked trees whose marked leaf is the (ℓ+1)-st vertex.

theorem PoissonDeclumping.PlaneTree.mem_cutFamily_iff {ℓ : ℕ} {A : MarkedTree} : A ∈ cutFamily ℓ ↔ A.pos = ℓ

noncomputable def PoissonDeclumping.PlaneTree.cutEquiv (ℓ : ℕ) : { T : PlaneTree // ℓ + 1 ≤ T.vertexCount } ≃ { A : MarkedTree // A.pos = ℓ } × PlaneTree

The cut-and-graft bijection {T : |T| ≥ ℓ + 1} ≃ 𝒜_ℓ × {plane trees}, T ↦ (Cut_ℓ(T), T_{u_{ℓ+1}(T)}), with inverse (A, S) ↦ A[S].

Equations

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

theorem PoissonDeclumping.PlaneTree.bienayme_cut_mem (μ : PMF ℕ) (ℓ : ℕ) (R : Set MarkedTree) (hR : R ⊆ cutFamily ℓ) (F : MarkedTree → Set PlaneTree) : (bienayme μ) {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ cut ℓ T ∈ R ∧ T.fringeAt ℓ ∈ F (cut ℓ T)} = ∑' (A : MarkedTree), R.indicator (fun (A : MarkedTree) => MarkedTree.weight μ A * (bienayme μ) (F A)) A

Sum over cut trees (inventory P18). For 𝓡 ⊆ 𝒜_ℓ and target sets F(A), 𝐏_μ(|𝒯| ≥ ℓ+1, Cut_ℓ(𝒯) ∈ 𝓡, 𝒯_{u_{ℓ+1}(𝒯)} ∈ F(Cut_ℓ(𝒯))) = ∑_{A ∈ 𝓡} w(A) 𝐏_μ(𝒯 ∈ F(A)), for every offspring law μ.