Size measures on rooted nonplanar trees and their forests

Main definitions

• RoseTree.leafCountP / RoseTree.leafDepthsP / RoseTree.leafDepthSumP (with Nonplanar descents): leaf statistics by predicate over the leaf projection — the count is Multiset.countP, and the depth statistics are the card and sum of the depth multiset (card_leafDepthsP).
• RootedTree.Nonplanar.numEdges: the edge count numNodes - 1 of a rooted tree.
• RootedTree.Forest.numNodes / RootedTree.Forest.numEdges: the forest totals.

Main results

• RootedTree.Forest.numNodes_eq_card_add_numEdges: Euler's relation #V = b₀ + #E for forests, with Multiset.card the component count.
• RoseTree.leafCountP_le_numNodes: a counted leaf is a vertex; strict when the root is uncounted (leafCountP_lt_numNodes_of_not).

[UPSTREAM] candidate alongside the Nonplanar carrier.

Leaf statistics by predicate

def RoseTree.leafCountP {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : ℕ

The number of leaves whose label satisfies p.

Equations

• RoseTree.leafCountP p t = Multiset.countP p t.leaves

def RoseTree.leafDepthsP {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : Multiset ℕ

The multiset of root-distances of the leaves whose label satisfies p.

Equations

• RoseTree.leafDepthsP p t = Multiset.map Prod.snd (Multiset.filter (fun (q : α × ℕ) => p q.1) t.leavesWithDepth)

def RoseTree.leafDepthSumP {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : ℕ

The sum of root-distances of the leaves whose label satisfies p.

Equations

• RoseTree.leafDepthSumP p t = (RoseTree.leafDepthsP p t).sum

@[simp]

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

@[simp]

theorem RoseTree.leafCountP_node_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : leafCountP p (node a (c :: cs)) = (List.map (leafCountP p) (c :: cs)).sum

theorem RoseTree.leafCountP_node_of_ne_nil {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) (h : cs ≠ []) : leafCountP p (node a cs) = (List.map (leafCountP p) cs).sum

On a non-leaf node the count is the children's total, for any root label.

theorem RoseTree.leafCountP_node_of_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) (h : ¬p a) : leafCountP p (node a cs) = (List.map (leafCountP p) cs).sum

A root failing p contributes nothing, for any child list.

theorem RoseTree.leafCountP_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {t : RoseTree α} : 0 < leafCountP p t ↔ ∃ (a : α), a ∈ t.leaves ∧ p a

theorem RoseTree.leafCountP_eq_zero {α : Type u_1} {p : α → Prop} [DecidablePred p] {t : RoseTree α} : leafCountP p t = 0 ↔ ∀ (a : α), a ∈ t.leaves → ¬p a

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

The count exhausts the leaves exactly when every leaf label satisfies p.

@[simp]

theorem RoseTree.card_leafDepthsP {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : (leafDepthsP p t).card = leafCountP p t

The counted leaves are exactly the depth entries: leafCountP is their number.

@[simp]

theorem RoseTree.leafDepthSumP_leaf {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : leafDepthSumP p (node a []) = 0

theorem RoseTree.leafDepthsP_node_cons {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : leafDepthsP p (node a (c :: cs)) = (List.map (fun (t : RoseTree α) => Multiset.map (fun (x : ℕ) => x + 1) (leafDepthsP p t)) (c :: cs)).sum

The counted-leaf depths of a node are the children's, each one edge deeper.

@[simp]

theorem RoseTree.leafDepthSumP_node {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) : leafDepthSumP p (node a cs) = (List.map (fun (c : RoseTree α) => leafDepthSumP p c + leafCountP p c) cs).sum

Each child contributes its own depth-weighted count plus one per counted leaf it carries (the extra edge from the node to the child).

theorem RoseTree.leafCountP_perm {α : Type u_1} (p : α → Prop) [DecidablePred p] {t s : RoseTree α} (h : t.Perm s) : leafCountP p t = leafCountP p s

leafCountP is a Perm-invariant.

theorem RoseTree.leafDepthsP_perm {α : Type u_1} (p : α → Prop) [DecidablePred p] {t s : RoseTree α} (h : t.Perm s) : leafDepthsP p t = leafDepthsP p s

leafDepthsP is a Perm-invariant.

theorem RoseTree.leafDepthSumP_perm {α : Type u_1} (p : α → Prop) [DecidablePred p] {t s : RoseTree α} (h : t.Perm s) : leafDepthSumP p t = leafDepthSumP p s

leafDepthSumP is a Perm-invariant.

theorem RoseTree.sum_map_leafCountP_le_node {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) : (List.map (leafCountP p) cs).sum ≤ leafCountP p (node a cs)

The children's counted leaves are bounded by the node's.

theorem RoseTree.leafCountP_le_numNodes {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : leafCountP p t ≤ t.numNodes

A counted leaf is a vertex: Multiset.countP_le_card through the leaf projection.

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

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

theorem RoseTree.leafCountP_le_leafDepthSumP_of_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (cs : List (RoseTree α)) (h : ¬p a) : leafCountP p (node a cs) ≤ leafDepthSumP p (node a cs)

A root failing p puts every counted leaf at depth ≥ 1, so the depth-weighted count dominates the plain count.

def RootedTree.Nonplanar.numEdges {α : Type u_1} (t : Nonplanar α) : ℕ

The number of edges of a rooted tree, numNodes - 1: every vertex except the root has exactly one parent edge.

Equations

• t.numEdges = t.numNodes - 1

@[simp]

theorem RootedTree.Nonplanar.numEdges_leaf {α : Type u_1} (a : α) : (leaf a).numEdges = 0

theorem RootedTree.Nonplanar.numEdges_eq_numNodes_sub_one {α : Type u_1} (t : Nonplanar α) : t.numEdges = t.numNodes - 1

theorem RootedTree.Nonplanar.numEdges_add_one {α : Type u_1} (t : Nonplanar α) : t.numEdges + 1 = t.numNodes

Euler's relation for a rooted tree: #V = 1 + #E.

theorem RootedTree.Nonplanar.numEdges_node {α : Type u_1} (a : α) (F : Multiset (Nonplanar α)) : (node a F).numEdges = (Multiset.map numNodes F).sum

The edges of a node are the root-to-child edges plus each child's own: the total vertex count of the children.

theorem RootedTree.Nonplanar.numEdges_node_pair {α : Type u_1} (a : α) (l r : Nonplanar α) : (node a {l, r}).numEdges = l.numEdges + r.numEdges + 2

Adjoining a root above a pair of trees adds two edges.

Leaf statistics by predicate, on the quotient

def RootedTree.Nonplanar.leafCountP {α : Type u_1} (p : α → Prop) [DecidablePred p] : Nonplanar α → ℕ

The number of leaves whose label satisfies p.

Equations

• RootedTree.Nonplanar.leafCountP p = RootedTree.Nonplanar.lift (RoseTree.leafCountP p) ⋯

@[simp]

theorem RootedTree.Nonplanar.leafCountP_mk {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : leafCountP p (mk t) = RoseTree.leafCountP p t

@[simp]

theorem RootedTree.Nonplanar.leafCountP_leaf {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : leafCountP p (leaf a) = if p a then 1 else 0

theorem RootedTree.Nonplanar.leafCountP_node_of_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (F : Multiset (Nonplanar α)) (h : ¬p a) : leafCountP p (node a F) = (Multiset.map (leafCountP p) F).sum

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

def RootedTree.Nonplanar.leafDepthSumP {α : Type u_1} (p : α → Prop) [DecidablePred p] : Nonplanar α → ℕ

The sum of root-distances of the leaves whose label satisfies p.

Equations

• RootedTree.Nonplanar.leafDepthSumP p = RootedTree.Nonplanar.lift (RoseTree.leafDepthSumP p) ⋯

@[simp]

theorem RootedTree.Nonplanar.leafDepthSumP_mk {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : RoseTree α) : leafDepthSumP p (mk t) = RoseTree.leafDepthSumP p t

@[simp]

theorem RootedTree.Nonplanar.leafDepthSumP_leaf {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) : leafDepthSumP p (leaf a) = 0

@[simp]

theorem RootedTree.Nonplanar.leafDepthSumP_node {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) (F : Multiset (Nonplanar α)) : leafDepthSumP p (node a F) = (Multiset.map (fun (c : Nonplanar α) => leafDepthSumP p c + leafCountP p c) F).sum

Each child contributes its own depth-weighted count plus one per counted leaf it carries.

theorem RootedTree.Nonplanar.leafCountP_lt_numNodes_of_not_root {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : Nonplanar α) (h : ¬p t.rootValue) : leafCountP p t < t.numNodes

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

theorem RootedTree.Nonplanar.leafCountP_le_leafDepthSumP_of_not_root {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : Nonplanar α) (h : ¬p t.rootValue) : leafCountP p t ≤ leafDepthSumP p t

A root failing p puts every counted leaf at depth ≥ 1.

theorem RootedTree.Nonplanar.leafCountP_le_numEdges {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : Nonplanar α) (h : leafCountP p t < t.numNodes) : leafCountP p t ≤ t.numEdges

Counted leaves are among the non-root vertices whenever some vertex is uncounted.

Forest measures

def RootedTree.Forest.numNodes {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

The total vertex count of a forest.

Equations

• RootedTree.Forest.numNodes F = (Multiset.map RootedTree.Nonplanar.numNodes F).sum

@[simp]

theorem RootedTree.Forest.numNodes_zero {α : Type u_1} : numNodes 0 = 0

@[simp]

theorem RootedTree.Forest.numNodes_cons {α : Type u_1} (T : Nonplanar α) (F : Multiset (Nonplanar α)) : numNodes (T ::ₘ F) = T.numNodes + numNodes F

@[simp]

theorem RootedTree.Forest.numNodes_singleton {α : Type u_1} (T : Nonplanar α) : numNodes {T} = T.numNodes

@[simp]

theorem RootedTree.Forest.numNodes_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : numNodes (F + G) = numNodes F + numNodes G

def RootedTree.Forest.numEdges {α : Type u_1} (F : Multiset (Nonplanar α)) : ℕ

The total edge count of a forest.

Equations

• RootedTree.Forest.numEdges F = (Multiset.map RootedTree.Nonplanar.numEdges F).sum

@[simp]

theorem RootedTree.Forest.numEdges_zero {α : Type u_1} : numEdges 0 = 0

@[simp]

theorem RootedTree.Forest.numEdges_cons {α : Type u_1} (T : Nonplanar α) (F : Multiset (Nonplanar α)) : numEdges (T ::ₘ F) = T.numEdges + numEdges F

@[simp]

theorem RootedTree.Forest.numEdges_singleton {α : Type u_1} (T : Nonplanar α) : numEdges {T} = T.numEdges

@[simp]

theorem RootedTree.Forest.numEdges_add {α : Type u_1} (F G : Multiset (Nonplanar α)) : numEdges (F + G) = numEdges F + numEdges G

theorem RootedTree.Forest.numNodes_eq_card_add_numEdges {α : Type u_1} (F : Multiset (Nonplanar α)) : numNodes F = F.card + numEdges F

Euler's relation for forests: #V = b₀ + #E, with Multiset.card the number of component trees.