Leaf projections of a rose tree

leavesWithDepth collects the leaves of a rose tree as a multiset of (label, root-distance) pairs; leaves forgets the depths. Leaf statistics are then Multiset computations — counts are Multiset.countP, bounds are inherited from Multiset.countP_le_card — instead of one bespoke fold per statistic.

Main definitions

• RoseTree.leavesWithDepth, RoseTree.leaves: the projections, with descents RootedTree.Nonplanar.leavesWithDepth and RootedTree.Nonplanar.leaves.

Main results

• RoseTree.card_leavesWithDepth: the projection has numLeaves elements.
• RoseTree.numLeaves_le_numNodes: a leaf is a vertex.

[UPSTREAM] candidate alongside the RoseTree carrier.

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

Depth-forgetting collapses the shift: the leaf labels of a node are the children's leaf labels.

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

The number of leaf labels is the number of leaves.

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 a Perm-invariant: 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.

Descent to Nonplanar

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

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

Equations

• RootedTree.Nonplanar.leavesWithDepth = RootedTree.Nonplanar.lift RoseTree.leavesWithDepth ⋯

@[simp]

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

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

The multiset of leaf labels of a nonplanar tree.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The projection has one element per leaf.

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

The number of leaf labels is the number of leaves.

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

A leaf is a vertex.