Leaf projections of a rose tree

RoseTree.leavesWithDepth collects the leaves of a rose tree as a multiset of pairs of a label and its distance from the root. RoseTree.leaves forgets the distances, which leaves the frontier RoseTree.leafList without its order. The number of leaves satisfying a predicate is Multiset.countP on leaves.

Main definitions

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

Main results

• RoseTree.card_leavesWithDepth: the projection has numLeaves elements.
• RoseTree.coe_leafList: the leaf labels are the frontier with its order forgotten.
• RoseTree.numLeaves_le_numNodes: a leaf is a vertex.
• RoseTree.countP_leaves_lt_numNodes_of_not: when the root fails the predicate, the counted leaves are among the non-root vertices.
• RoseTree.leavesWithDepth_perm, RoseTree.leaves_perm: both projections are Perm-invariant.

The projections

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

The leaves of a rose tree, each paired with its distance from the root.

Equations

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

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

The multiset of leaf labels of a rose tree.

Equations

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

@[simp]

theorem RoseTree.leavesWithDepth_leaf {α : Type u_1} (a : α) : (node a []).leavesWithDepth = {(a, 0)}

@[simp]

theorem RoseTree.leavesWithDepth_node_cons {α : Type u_1} (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : (node a (c :: cs)).leavesWithDepth = (List.map (fun (t : RoseTree α) => Multiset.map (fun (p : α × ℕ) => (p.1, p.2 + 1)) t.leavesWithDepth) (c :: cs)).sum

@[simp]

theorem RoseTree.leaves_leaf {α : Type u_1} (a : α) : (node a []).leaves = {a}

@[simp]

theorem RoseTree.leaves_node_cons {α : Type u_1} (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : (node a (c :: cs)).leaves = (List.map leaves (c :: cs)).sum

Cardinality

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

The projection has one element per leaf.

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

theorem RoseTree.coe_leafList {α : Type u_1} (t : RoseTree α) : ↑t.leafList = t.leaves

The leaf labels are the frontier with its order forgotten.

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

A leaf is a vertex.

Perm invariance

theorem RoseTree.leavesWithDepth_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.leavesWithDepth = s.leavesWithDepth

leavesWithDepth is Perm-invariant, since the fold algebra reads its arguments only through a nil test and a sum.

theorem RoseTree.leaves_perm {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : t.leaves = s.leaves

leaves is a Perm-invariant.

Leaf statistics by predicate

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

@[simp]

theorem RoseTree.countP_leaves_node_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : Multiset.countP p (node a (c :: cs)).leaves = (List.map (fun (t : RoseTree α) => Multiset.countP p t.leaves) (c :: cs)).sum

theorem RoseTree.countP_leaves_node_of_ne_nil {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) {cs : List (RoseTree α)} (h : cs ≠ []) : Multiset.countP p (node a cs).leaves = (List.map (fun (t : RoseTree α) => Multiset.countP p t.leaves) cs).sum

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

theorem RoseTree.countP_leaves_eq_numLeaves {α : Type u_1} (p : α → Prop) [DecidablePred p] {t : RoseTree α} : Multiset.countP p t.leaves = t.numLeaves ↔ ∀ (a : α), a ∈ t.leaves → p a

@[simp]

theorem RoseTree.card_filter_leavesWithDepth {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : (Multiset.filter (fun (q : α × ℕ) => p q.1) t.leavesWithDepth).card = Multiset.countP p t.leaves

theorem RoseTree.sum_map_countP_leaves_le_node {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) : (List.map (fun (t : RoseTree α) => Multiset.countP p t.leaves) cs).sum ≤ Multiset.countP p (node a cs).leaves

theorem RoseTree.countP_leaves_le_numNodes {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : Multiset.countP p t.leaves ≤ t.numNodes

theorem RoseTree.countP_leaves_lt_numNodes_of_not {α : Type u_1} (p : α → Prop) [DecidablePred p] {a : α} (cs : List (RoseTree α)) (h : ¬p a) : Multiset.countP p (node a cs).leaves < (node a cs).numNodes

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