Documentation

Linglib.Core.Combinatorics.RootedTree.Crown

Crowns of cuts #

A cut removes subtrees hanging below the root, so every crown component of a cut of T is a proper subtree of T. For a policy that allows a cut at every subtree the converse holds, since any one subtree below the root is removed by the cut at its own edge. Hence, for the pruning cuts, X is not a subtree of T exactly when T ≠ X and no cut of T has X in its crown.

Main results #

References #

Crown components are proper subtrees #

source
theorem ConnesKreimer.mk_mem_of_mem_crown_cutSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (p : Multiset (RoseTree α) × RoseTree α) :
p ∈ cutSummandsG extract t → ∀ x ∈ p.1, UnorderedTree.mk x ∈ RoseTree.unorderedSubtreesList t.children

Every crown component of a cut of t is a subtree of a child of t.

source
theorem ConnesKreimer.mk_mem_of_mem_crown_cutListSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (cs : List (RoseTree α)) (q : Multiset (RoseTree α) × List (RoseTree α)) :
q ∈ cutListSummandsG extract cs → ∀ x ∈ q.1, UnorderedTree.mk x ∈ RoseTree.unorderedSubtreesList cs

Every crown component of a cut of a list of children is a subtree of one of them.

source
theorem ConnesKreimer.mk_mem_of_mem_crown_augActionG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (a : Multiset (RoseTree α) × List (RoseTree α)) :
a ∈ augActionG extract t → ∀ x ∈ a.1, UnorderedTree.mk x ∈ t.unorderedSubtrees

Every crown component of a choice at the child t is a subtree of t.

Every proper subtree is a crown component #

This needs a policy that allows a cut at every subtree.

source
theorem ConnesKreimer.zero_mem_cutSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) :
(0, t) ∈ cutSummandsG extract t

The empty cut is a cut.

source
theorem ConnesKreimer.zero_mem_cutListSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (cs : List (RoseTree α)) :
(0, cs) ∈ cutListSummandsG extract cs

The empty cut is a cut of a list of children.

source
theorem ConnesKreimer.zero_mem_augActionG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) :
(0, [t]) ∈ augActionG extract t

Keeping the child whole is one of the choices at a child.

source
theorem ConnesKreimer.exists_mem_crown_cutSummandsG {α : Type u_1} {extract : RoseTree α → Option (List (RoseTree α))} (hex : ∀ (t : RoseTree α), (extract t).isSome = true) (t : RoseTree α) (s : UnorderedTree α) :
s ∈ RoseTree.unorderedSubtreesList t.children → ∃ p ∈ cutSummandsG extract t, ∃ x ∈ p.1, UnorderedTree.mk x = s

Every subtree of a child of t is a crown component of some cut of t.

source
theorem ConnesKreimer.exists_mem_crown_cutListSummandsG {α : Type u_1} {extract : RoseTree α → Option (List (RoseTree α))} (hex : ∀ (t : RoseTree α), (extract t).isSome = true) (cs : List (RoseTree α)) (s : UnorderedTree α) :
s ∈ RoseTree.unorderedSubtreesList cs → ∃ q ∈ cutListSummandsG extract cs, ∃ x ∈ q.1, UnorderedTree.mk x = s

Every subtree of a child in the list is a crown component of some cut of the list.

source
theorem ConnesKreimer.exists_mem_crown_augActionG {α : Type u_1} {extract : RoseTree α → Option (List (RoseTree α))} (hex : ∀ (t : RoseTree α), (extract t).isSome = true) (t : RoseTree α) (s : UnorderedTree α) :
s ∈ t.unorderedSubtrees → ∃ a ∈ augActionG extract t, ∃ x ∈ a.1, UnorderedTree.mk x = s

Every subtree of t is a crown component of some choice at the child t.

source
theorem ConnesKreimer.exists_mem_crown_cutSummandsN_iff {α : Type u_1} {T X : UnorderedTree α} :
(∃ p ∈ cutSummandsN T, X ∈ p.1) ↔ X ∈ T.subtrees ∧ X ≠ T

The crown components of the pruning cuts of T are exactly its proper subtrees.

source
theorem ConnesKreimer.not_mem_subtrees_iff {α : Type u_1} {T X : UnorderedTree α} :
X ∉ T.subtrees ↔ T ≠ X ∧ ∀ p ∈ cutSummandsN T, X ∉ p.1

X is not a subtree of T exactly when T ≠ X and no pruning cut of T has X in its crown.