Admissible-cut enumeration on rose trees

The combinatorics of admissible cuts, independent of the Hopf-algebra structures built on it in Core/Algebra/RootedTree/Coproduct/. An admissible cut of a tree removes a set of subtrees, no two on a common path to the root. It splits the tree into a crown, the multiset of removed subtrees, and a trunk, what is left at the root. The enumeration is parameterized by an extraction policy extract : RoseTree α → Option (List (RoseTree α)), called on each cut subtree:

• extract t = none forbids cuts at that subtree;
• extract t = some [] removes it, leaving nothing in the parent's child slot;
• extract t = some rs removes it and leaves the replacement trees rs in its slot.

The cut bookkeeping is shared by every policy; only the remainder left at a cut varies. The policy pruning, which always leaves nothing, gives the cuts of the Connes–Kreimer coproduct.

Main definitions

• ConnesKreimer.cutSummandsG extract: the enumeration of the pairs of a crown and a trunk.
• ConnesKreimer.ExtractInvariant: the policies that descend along RoseTree.Perm.
• ConnesKreimer.pruning, ConnesKreimer.cutSummandsN: the pruning policy and its cuts on UnorderedTree.
• ConnesKreimer.emptyCuts: the enumeration with only the empty cut.
• ConnesKreimer.CutChoice, ConnesKreimer.forestCutChoicesG cuts F: a cut chosen for each tree of a forest, with its crown, its trunk and the number of trees it takes whole.
• ConnesKreimer.CutChoice.HasExtractionCost: each tree the choice cuts measures its crown and its trunk and a fixed amount for each tree extracted.
• ConnesKreimer.countSingleCutsRho: the number of single cuts with given crown and trunk.

Main results

• ConnesKreimer.cutSummandsG_proj_perm: the projected enumeration is Perm-invariant for an invariant policy.
• ConnesKreimer.cutSummandsG_filter_empty: the empty cut is the unique cut with empty crown.
• ConnesKreimer.cutSummandsN_node: the pruning cuts of a node are the cut convolution over its children.
• ConnesKreimer.CutChoice.HasExtractionCost.sum_map_add_mul_numWhole: a choice of cuts keeps the measure of the forest up to its extraction cost.

[UPSTREAM] candidate.

References

• [CK98]
• [Foi]

The enumeration

@[irreducible]

def ConnesKreimer.cutSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Multiset (RoseTree α) × RoseTree α)

The cuts of a tree under the policy extract, as pairs of a crown and a trunk.

Equations

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

@[irreducible]

def ConnesKreimer.cutListSummandsG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : List (RoseTree α) → Multiset (Multiset (RoseTree α) × List (RoseTree α))

The cuts of a list of children, as pairs of a crown and the list of what remains. A surviving child contributes its trunk and a cut child contributes extract of it.

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.cutListSummandsG extract [] = {(0, [])}

@[irreducible]

def ConnesKreimer.augActionG {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : RoseTree α → Multiset (Multiset (RoseTree α) × List (RoseTree α))

The choices at one child t are to cut t itself, with crown {t} and remainder extract t when the policy allows it, or to cut inside t.

Equations

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

@[simp]

theorem ConnesKreimer.cutSummandsG_node {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (a : α) (cs : List (RoseTree α)) : cutSummandsG extract (RoseTree.node a cs) = Multiset.map (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => (p.1, RoseTree.node a p.2)) (cutListSummandsG extract cs)

@[simp]

theorem ConnesKreimer.cutListSummandsG_nil {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : cutListSummandsG extract [] = {(0, [])}

@[simp]

theorem ConnesKreimer.cutListSummandsG_cons {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (ts : List (RoseTree α)) : cutListSummandsG extract (t :: ts) = Multiset.map (fun (p : (Multiset (RoseTree α) × List (RoseTree α)) × Multiset (RoseTree α) × List (RoseTree α)) => (p.1.1 + p.2.1, p.1.2 ++ p.2.2)) (augActionG extract t ×ˢ cutListSummandsG extract ts)

@[simp]

theorem ConnesKreimer.augActionG_eq {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) : augActionG extract t = (match extract t with | none => 0 | some r => {({t}, r)}) + Multiset.map (fun (p : Multiset (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

theorem ConnesKreimer.augActionG_eq_none {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (h : extract t = none) : augActionG extract t = Multiset.map (fun (p : Multiset (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Where the policy forbids a cut, the only choices at a child are the cuts inside it.

theorem ConnesKreimer.augActionG_eq_some {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) (r : List (RoseTree α)) (h : extract t = some r) : augActionG extract t = ({t}, r) ::ₘ Multiset.map (fun (p : Multiset (RoseTree α) × RoseTree α) => (p.1, [p.2])) (cutSummandsG extract t)

Where the policy allows a cut, cutting the child itself is one of the choices.

Vertex conservation

When every remainder the policy leaves has k vertices in total, a cut conserves vertices up to k per crown component. Pruning has k = 0 and a policy leaving one leaf has k = 1.

theorem ConnesKreimer.cutSummandsG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) {k : ℕ} (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = k) (t : RoseTree α) (p : Multiset (RoseTree α) × RoseTree α) : p ∈ cutSummandsG extract t → (Multiset.map RoseTree.numNodes p.1).sum + p.2.numNodes = t.numNodes + k * p.1.card

The crown and the trunk of a cut have the vertices of the tree, plus k for each crown component.

theorem ConnesKreimer.cutListSummandsG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) {k : ℕ} (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = k) (cs : List (RoseTree α)) (q : Multiset (RoseTree α) × List (RoseTree α)) : q ∈ cutListSummandsG extract cs → (Multiset.map RoseTree.numNodes q.1).sum + (List.map RoseTree.numNodes q.2).sum = (List.map RoseTree.numNodes cs).sum + k * q.1.card

theorem ConnesKreimer.augActionG_numNodes {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) {k : ℕ} (hext : ∀ (t : RoseTree α) (r : List (RoseTree α)), extract t = some r → (List.map RoseTree.numNodes r).sum = k) (t : RoseTree α) (a : Multiset (RoseTree α) × List (RoseTree α)) : a ∈ augActionG extract t → (Multiset.map RoseTree.numNodes a.1).sum + (List.map RoseTree.numNodes a.2).sum = t.numNodes + k * a.1.card

Projection to unordered trees

A cut of a rose tree projects to UnorderedTree componentwise. On children the remainder list becomes a multiset, and the combination of the cuts of two children becomes combinerProjG.

def ConnesKreimer.projSummand {α : Type u_1} (p : Multiset (RoseTree α) × RoseTree α) : Multiset (UnorderedTree α) × UnorderedTree α

Project the crown and the trunk of a cut to unordered trees.

Equations

• ConnesKreimer.projSummand p = (Multiset.map UnorderedTree.mk p.1, UnorderedTree.mk p.2)

def ConnesKreimer.projForest {α : Type u_1} (p : Multiset (RoseTree α) × List (RoseTree α)) : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)

Project the crown and the remainder list of a cut of a list of children.

Equations

• ConnesKreimer.projForest p = (Multiset.map UnorderedTree.mk p.1, ↑(List.map UnorderedTree.mk p.2))

theorem ConnesKreimer.projSummand_node {α : Type u_1} (a : α) (p : Multiset (RoseTree α) × List (RoseTree α)) : projSummand (p.1, RoseTree.node a p.2) = ((projForest p).1, UnorderedTree.node a (projForest p).2)

def ConnesKreimer.combinerProjG {α : Type u_1} : (Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) × Multiset (UnorderedTree α) × Multiset (UnorderedTree α) → Multiset (UnorderedTree α) × Multiset (UnorderedTree α)

Combine two pairs of a crown and a remainder by adding componentwise.

Equations

• ConnesKreimer.combinerProjG ((F1, m1), F2, m2) = (F1 + F2, m1 + m2)

Policies that descend to unordered trees

def ConnesKreimer.ExtractInvariant {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) : Prop

A policy is invariant when the projection of what it leaves at a cut depends only on the unordered tree that is cut.

Equations

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

theorem ConnesKreimer.combinerProjG_swap_args {α : Type u_1} (a b c : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) : combinerProjG (a, combinerProjG (b, c)) = combinerProjG (b, combinerProjG (a, c))

Combining three pairs is symmetric in the first two.

theorem ConnesKreimer.swap_double_combinerProjG {α : Type u_1} (A B C : Multiset (Multiset (UnorderedTree α) × Multiset (UnorderedTree α))) : Multiset.map combinerProjG (A ×ˢ Multiset.map combinerProjG (B ×ˢ C)) = Multiset.map combinerProjG (B ×ˢ Multiset.map combinerProjG (A ×ˢ C))

The combination of three multisets of pairs is symmetric in the first two.

theorem ConnesKreimer.cutSummandsG_proj_perm {α : Type u_1} {extract : RoseTree α → Option (List (RoseTree α))} (hExt : ExtractInvariant extract) {t s : RoseTree α} : t.Perm s → Multiset.map projSummand (cutSummandsG extract t) = Multiset.map projSummand (cutSummandsG extract s)

For an invariant policy, the projected cuts of a tree depend only on the unordered tree.

Cut convolution

treeCutsG cuts T lists the cuts of the tree T as a forest, including the cut that takes all of T, and forestCutsG cuts F combines them over the trees of a forest. The admissible-cut coproduct is a sum over these (comulForestNG_eq_sum in Coproduct/WithCuts.lean).

def ConnesKreimer.treeCutsG {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) : Multiset (Multiset (UnorderedTree α) × Multiset (UnorderedTree α))

All the cuts of a tree with the trunk as a forest. They are the cut taking the whole tree, with crown {T} and empty trunk, and each cut in cuts T with a one-tree trunk.

Equations

• ConnesKreimer.treeCutsG cuts T = ({T}, 0) ::ₘ Multiset.map (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => (p.1, {p.2})) (cuts T)

instance ConnesKreimer.instLeftCommConvCut {α : Type u_1} : LeftCommutative fun (s acc : Multiset (Multiset (UnorderedTree α) × Multiset (UnorderedTree α))) => Multiset.map combinerProjG (s ×ˢ acc)

def ConnesKreimer.forestCutsG {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (F : Multiset (UnorderedTree α)) : Multiset (Multiset (UnorderedTree α) × Multiset (UnorderedTree α))

The cuts of a forest combine one choice from treeCutsG cuts T for each tree T.

Equations

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

theorem ConnesKreimer.forestCutsG_zero {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : forestCutsG cuts 0 = {(0, 0)}

theorem ConnesKreimer.forestCutsG_cons {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) (F : Multiset (UnorderedTree α)) : forestCutsG cuts (T ::ₘ F) = Multiset.map combinerProjG (treeCutsG cuts T ×ˢ forestCutsG cuts F)

theorem ConnesKreimer.forestCutsG_singleton {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) : forestCutsG cuts {T} = treeCutsG cuts T

theorem ConnesKreimer.forestCutsG_pair {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (T T' : UnorderedTree α) : forestCutsG cuts {T, T'} = Multiset.map combinerProjG (treeCutsG cuts T ×ˢ treeCutsG cuts T')

Cuts chosen tree by tree

A CutChoice records, for each tree of a forest, the crown and trunk of the cut chosen for it beside the tree, and forestCutChoicesG cuts F lists the choices for F. Gathering the crowns and the trunks of a choice gives a forest cut of F (forestCutsG_eq_map_forestCutChoicesG), and the record says where each tree went: into the crown whole, or cut and left as a trunk.

@[reducible, inline]

abbrev ConnesKreimer.CutChoice (α : Type u_2) : Type u_2

A choice of cuts for the trees of a forest, each tree beside the crown and the trunk of the cut chosen for it.

Equations

• ConnesKreimer.CutChoice α = Multiset (UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α))

def ConnesKreimer.CutChoice.crown {α : Type u_1} (s : CutChoice α) : Multiset (UnorderedTree α)

The crown of a choice of cuts gathers the crowns chosen for its trees.

Equations

• s.crown = (Multiset.map Prod.snd s).sum.1

def ConnesKreimer.CutChoice.trunk {α : Type u_1} (s : CutChoice α) : Multiset (UnorderedTree α)

The trunk of a choice of cuts gathers the trunks its trees leave.

Equations

• s.trunk = (Multiset.map Prod.snd s).sum.2

def ConnesKreimer.CutChoice.numWhole {α : Type u_1} [DecidableEq (UnorderedTree α)] (s : CutChoice α) : ℕ

The number of trees a choice of cuts takes whole, leaving no trunk.

Equations

• s.numWhole = Multiset.countP (fun (x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => x.2.2 = 0) s

@[simp]

theorem ConnesKreimer.CutChoice.crown_zero {α : Type u_1} : crown 0 = 0

@[simp]

theorem ConnesKreimer.CutChoice.trunk_zero {α : Type u_1} : trunk 0 = 0

@[simp]

theorem ConnesKreimer.CutChoice.crown_cons {α : Type u_1} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} : crown (x ::ₘ s) = x.2.1 + s.crown

@[simp]

theorem ConnesKreimer.CutChoice.trunk_cons {α : Type u_1} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} : trunk (x ::ₘ s) = x.2.2 + s.trunk

@[simp]

theorem ConnesKreimer.CutChoice.crown_add {α : Type u_1} {s t : CutChoice α} : (s + t).crown = s.crown + t.crown

@[simp]

theorem ConnesKreimer.CutChoice.trunk_add {α : Type u_1} {s t : CutChoice α} : (s + t).trunk = s.trunk + t.trunk

@[simp]

theorem ConnesKreimer.CutChoice.crown_singleton {α : Type u_1} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} : {x}.crown = x.2.1

@[simp]

theorem ConnesKreimer.CutChoice.trunk_singleton {α : Type u_1} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} : {x}.trunk = x.2.2

theorem ConnesKreimer.CutChoice.mem_crown {α : Type u_1} {s : CutChoice α} {T : UnorderedTree α} : T ∈ s.crown ↔ ∃ (x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)), x ∈ s ∧ T ∈ x.2.1

theorem ConnesKreimer.CutChoice.mem_trunk {α : Type u_1} {s : CutChoice α} {T : UnorderedTree α} : T ∈ s.trunk ↔ ∃ (x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)), x ∈ s ∧ T ∈ x.2.2

@[simp]

theorem ConnesKreimer.CutChoice.numWhole_zero {α : Type u_1} [DecidableEq (UnorderedTree α)] : numWhole 0 = 0

@[simp]

theorem ConnesKreimer.CutChoice.numWhole_cons {α : Type u_1} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} [DecidableEq (UnorderedTree α)] : numWhole (x ::ₘ s) = s.numWhole + if x.2.2 = 0 then 1 else 0

@[simp]

theorem ConnesKreimer.CutChoice.numWhole_singleton {α : Type u_1} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} [DecidableEq (UnorderedTree α)] : {x}.numWhole = if x.2.2 = 0 then 1 else 0

@[simp]

theorem ConnesKreimer.CutChoice.numWhole_add {α : Type u_1} {s t : CutChoice α} [DecidableEq (UnorderedTree α)] : (s + t).numWhole = s.numWhole + t.numWhole

theorem ConnesKreimer.CutChoice.numWhole_eq_zero {α : Type u_1} {s : CutChoice α} [DecidableEq (UnorderedTree α)] : s.numWhole = 0 ↔ ∀ (x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)), x ∈ s → x.2.2 ≠ 0

def ConnesKreimer.CutChoice.HasExtractionCost {α : Type u_1} (μ : UnorderedTree α → ℕ) (k : ℕ) (s : CutChoice α) : Prop

A choice of cuts has extraction cost k in a measure μ when each tree it cuts rather than takes whole measures its crown and its trunk together, and k more for each tree it extracts.

Equations

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

def ConnesKreimer.forestCutChoicesG {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (F : Multiset (UnorderedTree α)) : Multiset (CutChoice α)

The ways of choosing one cut of treeCutsG cuts T for each tree T of a forest.

Equations

• ConnesKreimer.forestCutChoicesG cuts F = (Multiset.map (fun (T : UnorderedTree α) => Multiset.map (Prod.mk T) (ConnesKreimer.treeCutsG cuts T)) F).Sections

theorem ConnesKreimer.forestCutChoicesG_zero {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : forestCutChoicesG cuts 0 = {0}

theorem ConnesKreimer.forestCutChoicesG_cons {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) (F : Multiset (UnorderedTree α)) : forestCutChoicesG cuts (T ::ₘ F) = (treeCutsG cuts T).bind fun (a : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => Multiset.map (fun (x : Multiset (UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α))) => (T, a) ::ₘ x) (forestCutChoicesG cuts F)

theorem ConnesKreimer.forestCutsG_eq_map_forestCutChoicesG {α : Type u_1} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) (F : Multiset (UnorderedTree α)) : forestCutsG cuts F = Multiset.map (fun (s : CutChoice α) => (s.crown, s.trunk)) (forestCutChoicesG cuts F)

Gathering the crowns and the trunks of a choice of cuts gives a forest cut, and every forest cut arises this way.

theorem ConnesKreimer.mem_treeCutsG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {T : UnorderedTree α} {a : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} : a ∈ treeCutsG cuts T ↔ a = ({T}, 0) ∨ ∃ (p : Multiset (UnorderedTree α) × UnorderedTree α), p ∈ cuts T ∧ (p.1, {p.2}) = a

A cut of a tree takes the whole tree into the crown, or cuts it and leaves one trunk.

theorem ConnesKreimer.map_fst_of_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} (hs : s ∈ forestCutChoicesG cuts F) : Multiset.map Prod.fst s = F

theorem ConnesKreimer.fst_mem_of_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} (hs : s ∈ forestCutChoicesG cuts F) (hx : x ∈ s) : x.1 ∈ F

theorem ConnesKreimer.mem_treeCutsG_of_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} (hs : s ∈ forestCutChoicesG cuts F) (hx : x ∈ s) : x.2 ∈ treeCutsG cuts x.1

theorem ConnesKreimer.snd_eq_of_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} (hs : s ∈ forestCutChoicesG cuts F) (hx : x ∈ s) (h : x.2.2 = 0) : x.2 = ({x.1}, 0)

A tree that leaves no trunk was taken whole into the crown.

theorem ConnesKreimer.CutChoice.fst_mem_crown {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} (hs : s ∈ forestCutChoicesG cuts F) (hx : x ∈ s) (h : x.2.2 = 0) : x.1 ∈ s.crown

A tree taken whole lies in the crown.

theorem ConnesKreimer.CutChoice.HasExtractionCost.of_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {μ : UnorderedTree α → ℕ} {k : ℕ} (hs : s ∈ forestCutChoicesG cuts F) (h : ∀ (x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)), x ∈ s → ∀ (p : Multiset (UnorderedTree α) × UnorderedTree α), p ∈ cuts x.1 → (p.1, {p.2}) = x.2 → μ x.1 = (Multiset.map μ p.1).sum + μ p.2 + k * p.1.card) : HasExtractionCost μ k s

A choice has extraction cost k when each cut it makes does.

theorem ConnesKreimer.CutChoice.card_trunk_add_numWhole {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} [DecidableEq (UnorderedTree α)] (hs : s ∈ forestCutChoicesG cuts F) : s.trunk.card + s.numWhole = F.card

Every tree of a forest leaves one trunk, except the trees taken whole into the crown.

theorem ConnesKreimer.CutChoice.card_add_numWhole_le_card_crown {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} {x : UnorderedTree α × Multiset (UnorderedTree α) × Multiset (UnorderedTree α)} [DecidableEq (UnorderedTree α)] (hs : s ∈ forestCutChoicesG cuts F) (hx : x ∈ s) (h : x.2.2 ≠ 0) : x.2.1.card + s.numWhole ≤ s.crown.card

The crown of a tree that is cut lies in the crown of the choice beside the trees taken whole.

theorem ConnesKreimer.CutChoice.HasExtractionCost.sum_map_add_mul_numWhole {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} {s : CutChoice α} [DecidableEq (UnorderedTree α)] {μ : UnorderedTree α → ℕ} {k : ℕ} (hs : s ∈ forestCutChoicesG cuts F) (hc : HasExtractionCost μ k s) : (Multiset.map μ F).sum + k * s.numWhole = (Multiset.map μ s.crown).sum + (Multiset.map μ s.trunk).sum + k * s.crown.card

A choice of cuts with extraction cost k in μ keeps the measure of the forest, counting k for each tree it extracts and each tree it takes whole as extracting itself.

theorem ConnesKreimer.add_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F G : Multiset (UnorderedTree α)} {s t : CutChoice α} (hs : s ∈ forestCutChoicesG cuts F) (ht : t ∈ forestCutChoicesG cuts G) : s + t ∈ forestCutChoicesG cuts (F + G)

Choices of cuts for two forests combine to a choice for their sum.

theorem ConnesKreimer.map_whole_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} (F : Multiset (UnorderedTree α)) : Multiset.map (fun (T : UnorderedTree α) => (T, {T}, 0)) F ∈ forestCutChoicesG cuts F

Every tree of a forest can be taken whole.

theorem ConnesKreimer.map_uncut_mem_forestCutChoicesG {α : Type u_1} {cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)} {F : Multiset (UnorderedTree α)} (h : ∀ (T : UnorderedTree α), T ∈ F → (0, T) ∈ cuts T) : Multiset.map (fun (T : UnorderedTree α) => (T, 0, {T})) F ∈ forestCutChoicesG cuts F

Every tree of a forest can be left uncut, when the empty cut is among its cuts.

@[simp]

theorem ConnesKreimer.CutChoice.crown_map_whole {α : Type u_1} (F : Multiset (UnorderedTree α)) : crown (Multiset.map (fun (T : UnorderedTree α) => (T, {T}, 0)) F) = F

Taking every tree of a forest whole puts the forest in the crown.

@[simp]

theorem ConnesKreimer.CutChoice.trunk_map_whole {α : Type u_1} (F : Multiset (UnorderedTree α)) : trunk (Multiset.map (fun (T : UnorderedTree α) => (T, {T}, 0)) F) = 0

@[simp]

theorem ConnesKreimer.CutChoice.numWhole_map_whole {α : Type u_1} (F : Multiset (UnorderedTree α)) [DecidableEq (UnorderedTree α)] : numWhole (Multiset.map (fun (T : UnorderedTree α) => (T, {T}, 0)) F) = F.card

@[simp]

theorem ConnesKreimer.CutChoice.crown_map_uncut {α : Type u_1} (F : Multiset (UnorderedTree α)) : crown (Multiset.map (fun (T : UnorderedTree α) => (T, 0, {T})) F) = 0

Leaving every tree of a forest uncut puts the forest in the trunk.

@[simp]

theorem ConnesKreimer.CutChoice.trunk_map_uncut {α : Type u_1} (F : Multiset (UnorderedTree α)) : trunk (Multiset.map (fun (T : UnorderedTree α) => (T, 0, {T})) F) = F

theorem ConnesKreimer.CutChoice.hasExtractionCost_map_whole {α : Type u_1} (F : Multiset (UnorderedTree α)) (μ : UnorderedTree α → ℕ) (k : ℕ) : HasExtractionCost μ k (Multiset.map (fun (T : UnorderedTree α) => (T, {T}, 0)) F)

A choice taking every tree whole extracts nothing, so it has every extraction cost.

The empty cut

theorem ConnesKreimer.cutSummandsG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (T : RoseTree α) : Multiset.filter (fun (p : Multiset (RoseTree α) × RoseTree α) => p.1.card = 0) (cutSummandsG extract T) = {(0, T)}

The empty cut is the unique cut with empty crown.

theorem ConnesKreimer.cutListSummandsG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (cs : List (RoseTree α)) : Multiset.filter (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => p.1.card = 0) (cutListSummandsG extract cs) = {(0, cs)}

The empty cut is the unique cut of a list of children with empty crown.

theorem ConnesKreimer.augActionG_filter_empty {α : Type u_1} (extract : RoseTree α → Option (List (RoseTree α))) (t : RoseTree α) : Multiset.filter (fun (p : Multiset (RoseTree α) × List (RoseTree α)) => p.1.card = 0) (augActionG extract t) = {(0, [t])}

Keeping the child whole is the unique choice at a child with empty crown.

Pruning cuts

The policy that leaves nothing at a cut gives the admissible cuts of the Connes–Kreimer coproduct. It is invariant, so its cuts descend to UnorderedTree, where the cuts of a node are the cut convolution over its children.

def ConnesKreimer.pruning {α : Type u_1} : RoseTree α → Option (List (RoseTree α))

The pruning policy cuts anywhere and leaves nothing in place of the cut subtree.

Equations

• ConnesKreimer.pruning x✝ = some []

theorem ConnesKreimer.extractInvariant_pruning {α : Type u_1} : ExtractInvariant pruning

def ConnesKreimer.cutSummandsN {α : Type u_1} : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)

The pruning cuts of an unordered tree, as pairs of a crown and a trunk.

Equations

• ConnesKreimer.cutSummandsN = Quotient.lift (fun (T : RoseTree α) => Multiset.map ConnesKreimer.projSummand (ConnesKreimer.cutSummandsG ConnesKreimer.pruning T)) ⋯

@[simp]

theorem ConnesKreimer.cutSummandsN_mk {α : Type u_1} (T : RoseTree α) : cutSummandsN (UnorderedTree.mk T) = Multiset.map projSummand (cutSummandsG pruning T)

theorem ConnesKreimer.cutSummandsN_leaf {α : Type u_1} (a : α) : cutSummandsN (UnorderedTree.leaf a) = {(0, UnorderedTree.leaf a)}

A leaf has only the empty cut.

def ConnesKreimer.countSingleCutsRho {α : Type u_1} [DecidableEq α] (T T₁ T₂ : UnorderedTree α) : ℕ

The number of pruning cut summands of T whose crown is {T₁} and whose trunk is T₂.

Equations

• ConnesKreimer.countSingleCutsRho T T₁ T₂ = Multiset.countP (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => p.1 = {T₁} ∧ p.2 = T₂) (ConnesKreimer.cutSummandsN T)

@[simp]

theorem ConnesKreimer.cutSummandsN_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : cutSummandsN (UnorderedTree.node a F) = Multiset.map (fun (pf : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (pf.1, UnorderedTree.node a pf.2)) (forestCutsG cutSummandsN F)

The pruning cuts of a node choose, for each child, to cut it whole or to cut inside it.

def ConnesKreimer.emptyCuts {α : Type u_1} (T : UnorderedTree α) : Multiset (Multiset (UnorderedTree α) × UnorderedTree α)

The enumeration whose only cut is the empty cut. Its coproduct makes every tree primitive.

Equations

• ConnesKreimer.emptyCuts T = {(0, T)}

theorem ConnesKreimer.forestCutsG_emptyCuts {α : Type u_1} (F : Multiset (UnorderedTree α)) : forestCutsG emptyCuts F = F.antidiagonal

The forest cuts of the empty-cut enumeration split a forest into two subforests.

theorem ConnesKreimer.cutSummandsN_filter_empty {α : Type u_1} (T : UnorderedTree α) : Multiset.filter (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => p.1.card = 0) (cutSummandsN T) = {(0, T)}

The empty cut is the unique pruning cut with empty crown.