Leaf projections of an unordered tree

RoseTree.leavesWithDepth and RoseTree.leaves are Perm-invariant, so they descend to the quotient, and the leaf statistics by predicate descend with them.

Main definitions

• UnorderedTree.leavesWithDepth, UnorderedTree.leaves: the projections.

Main results

• UnorderedTree.card_leaves: the projection has numLeaves elements.
• UnorderedTree.countP_leaves_lt_numNodes_of_not_root: when the root fails the predicate, the counted leaves are among the non-root vertices.

def UnorderedTree.leavesWithDepth {α : Type u_1} : UnorderedTree α → Multiset (α × ℕ)

The leaves of an unordered tree, each paired with its distance from the root.

Equations

• UnorderedTree.leavesWithDepth = Quotient.lift RoseTree.leavesWithDepth ⋯

@[simp]

theorem UnorderedTree.leavesWithDepth_mk {α : Type u_1} (t : RoseTree α) : (mk t).leavesWithDepth = t.leavesWithDepth

def UnorderedTree.leaves {α : Type u_1} (t : UnorderedTree α) : Multiset α

The multiset of leaf labels of an unordered tree.

Equations

• t.leaves = Multiset.map Prod.fst t.leavesWithDepth

@[simp]

theorem UnorderedTree.leaves_mk {α : Type u_1} (t : RoseTree α) : (mk t).leaves = t.leaves

@[simp]

theorem UnorderedTree.leavesWithDepth_leaf {α : Type u_1} (a : α) : (leaf a).leavesWithDepth = {(a, 0)}

@[simp]

theorem UnorderedTree.leaves_leaf {α : Type u_1} (a : α) : (leaf a).leaves = {a}

theorem UnorderedTree.card_leavesWithDepth {α : Type u_1} (t : UnorderedTree α) : t.leavesWithDepth.card = t.numLeaves

The projection has one element per leaf.

theorem UnorderedTree.card_leaves {α : Type u_1} (t : UnorderedTree α) : t.leaves.card = t.numLeaves

The number of leaf labels is the number of leaves.

theorem UnorderedTree.numLeaves_le_numNodes {α : Type u_1} (t : UnorderedTree α) : t.numLeaves ≤ t.numNodes

A leaf is a vertex.

theorem UnorderedTree.leaves_node_cons {α : Type u_1} (a : α) (T : UnorderedTree α) (cs : Multiset (UnorderedTree α)) : (node a (T ::ₘ cs)).leaves = T.leaves + (Multiset.map leaves cs).sum

The leaf labels of a branching node are the concatenation of its children's, as in RoseTree.leaves_node_cons.

Leaf statistics by predicate

theorem UnorderedTree.countP_leaves_leaf {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : Multiset.countP p (leaf a).leaves = if p a then 1 else 0

theorem UnorderedTree.countP_leaves_node_of_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (F : Multiset (UnorderedTree α)) (h : ¬p a) : Multiset.countP p (node a F).leaves = (Multiset.map (fun (T : UnorderedTree α) => Multiset.countP p T.leaves) F).sum

A root failing p contributes nothing, so the count is the children's total.

theorem UnorderedTree.countP_leaves_lt_numNodes_of_not_root {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : UnorderedTree α) (h : ¬p t.value) : Multiset.countP p t.leaves < t.numNodes

A root failing p is an uncounted vertex, so the count is strict.