Finite plane trees and marked fringe counts

Finite rooted ordered trees, as in Section 2.1 of the paper. The list of fringe trees records one entry for each vertex in depth-first order. Equal subtrees at different vertices remain separate entries, so counting does not lose multiplicity.

The definitions PlaneTree, children, rootDegree, fringeTrees, vertexCount, markCount and declumpedMark are in PoissonDeclumping.Statements.Defs, from the upstream statement contract; this file proves their basic properties.

def PoissonDeclumping.PlaneTree.PropagatesOutside (B : Set ℕ) (G : PlaneTree → Prop) : Prop

The propagation hypothesis in Lemma lem:declump_to_raw, for a fixed mark.

Equations

• PoissonDeclumping.PlaneTree.PropagatesOutside B G = ∀ (T U : PoissonDeclumping.PlaneTree), U ∈ T.children → G U → T.rootDegree ∉ B → G T

@[simp]

theorem PoissonDeclumping.PlaneTree.children_node (ts : List PlaneTree) : (node ts).children = ts

@[simp]

theorem PoissonDeclumping.PlaneTree.rootDegree_node (ts : List PlaneTree) : (node ts).rootDegree = ts.length

@[simp]

theorem PoissonDeclumping.PlaneTree.fringeTrees_node (ts : List PlaneTree) : (node ts).fringeTrees = node ts :: List.flatMap fringeTrees ts

theorem PoissonDeclumping.PlaneTree.self_mem_fringeTrees (T : PlaneTree) : T ∈ T.fringeTrees

The root contributes its own fringe tree.

theorem PoissonDeclumping.PlaneTree.mem_fringeTrees_of_mem_child {T U V : PlaneTree} (hU : U ∈ T.children) (hV : V ∈ U.fringeTrees) : V ∈ T.fringeTrees

A child fringe occurrence remains a fringe occurrence in the parent.

theorem PoissonDeclumping.PlaneTree.child_mem_fringeTrees {T U : PlaneTree} (hU : U ∈ T.children) : U ∈ T.fringeTrees

Every child itself occurs among the parent's fringe trees.

theorem PoissonDeclumping.PlaneTree.markCount_pos_iff (G : PlaneTree → Prop) (T : PlaneTree) : 0 < markCount G T ↔ ∃ U ∈ T.fringeTrees, G U

A positive marked count is exactly the existence of a marked vertex.

theorem PoissonDeclumping.PlaneTree.markCount_eq_zero_iff (G : PlaneTree → Prop) (T : PlaneTree) : markCount G T = 0 ↔ ∀ U ∈ T.fringeTrees, ¬G U

A zero marked count is exactly the absence of a marked vertex.

theorem PoissonDeclumping.PlaneTree.markCount_pos_of_root {G : PlaneTree → Prop} {T : PlaneTree} (h : G T) : 0 < markCount G T

Marking the root ensures that the raw count is positive.

theorem PoissonDeclumping.PlaneTree.markCount_pos_of_child {G : PlaneTree → Prop} {T U : PlaneTree} (hU : U ∈ T.children) (h : 0 < markCount G U) : 0 < markCount G T

A positive count in a child ensures a positive count in the parent.

theorem PoissonDeclumping.PlaneTree.induction_children {P : PlaneTree → Prop} (step : ∀ (T : PlaneTree), (∀ U ∈ T.children, P U) → P T) (T : PlaneTree) : P T

Structural induction with an induction hypothesis for every child.

theorem PoissonDeclumping.PlaneTree.mem_fringeTrees_trans {T U V : PlaneTree} (hU : U ∈ T.fringeTrees) (hV : V ∈ U.fringeTrees) : V ∈ T.fringeTrees

Fringe containment is transitive.

theorem PoissonDeclumping.PlaneTree.markCount_pos_iff_root_or_child (G : PlaneTree → Prop) (T : PlaneTree) : 0 < markCount G T ↔ G T ∨ ∃ U ∈ T.children, 0 < markCount G U

Any marked vertex is either the root or belongs to a child tree.