Documentation

HopfAlgebras.Forests.Rooted

Rooted Forests #

This file defines non-planar rooted forests as multisets of non-planar rooted trees. These are the monomials in the commutative algebra of rooted forests.

Main definitions #

RootedForest - non-planar rooted forests
RootedTree.branches - the forest immediately below the root
RootedForest.graft - the B_+ operator grafting a forest onto a new root
RootedForest.order - total number of vertices
RootedForest.treeFactorial - product of tree factorials

References #

John C. Butcher, Numerical Methods for Ordinary Differential Equations
Philippe Chartier, Ernst Hairer, Gilles Vilmart, Algebraic Structures of B-series

@[reducible, inline]

abbrev HopfAlgebras.RootedForest :

Non-planar rooted forests, represented by multisets of non-planar rooted trees.

Equations

HopfAlgebras.RootedForest = Multiset HopfAlgebras.RootedTree

Instances For

def HopfAlgebras.PTree.ForestPerm (ts us : List PTree) :

Two planar tree lists represent the same non-planar rooted forest.

Equations

HopfAlgebras.PTree.ForestPerm ts us = (↑(List.map HopfAlgebras.RootedTree.ofPTree ts) = ↑(List.map HopfAlgebras.RootedTree.ofPTree us))

Instances For

theorem HopfAlgebras.PTree.ForestPerm.refl (ts : List PTree) :

ForestPerm ts ts

theorem HopfAlgebras.PTree.ForestPerm.symm {ts us : List PTree} (h : ForestPerm ts us) :

ForestPerm us ts

theorem HopfAlgebras.PTree.ForestPerm.trans {ts us vs : List PTree} (h₁ : ForestPerm ts us) (h₂ : ForestPerm us vs) :

ForestPerm ts vs

theorem HopfAlgebras.PTree.ForestPerm.of_list_perm {ts us : List PTree} (h : ts.Perm us) :

ForestPerm ts us

theorem HopfAlgebras.PTree.ForestPerm.of_forall₂_perm {ts us : List PTree} (h : List.Forall₂ Perm ts us) :

ForestPerm ts us

theorem HopfAlgebras.PTree.ForestPerm.cons_eq {t u : PTree} {ts us : List PTree} (ht : RootedTree.ofPTree t = RootedTree.ofPTree u) (h : ForestPerm ts us) :

ForestPerm (t :: ts) (u :: us)

theorem HopfAlgebras.PTree.ForestPerm.cons {t u : PTree} {ts us : List PTree} (ht : t.Perm u) (h : ForestPerm ts us) :

ForestPerm (t :: ts) (u :: us)

theorem HopfAlgebras.PTree.ForestPerm.append {ts us vs ws : List PTree} (h₁ : ForestPerm ts us) (h₂ : ForestPerm vs ws) :

ForestPerm (ts ++ vs) (us ++ ws)

def HopfAlgebras.RootedTree.branches :

RootedTree → RootedForest

The forest immediately below the root of a non-planar rooted tree.

Equations

HopfAlgebras.RootedTree.branches = Quotient.lift HopfAlgebras.RootedTree.branchesAux✝ ⋯

Instances For

@[simp]

theorem HopfAlgebras.RootedTree.branches_ofPTree_node (ts : List PTree) :

(ofPTree (PTree.node ts)).branches = ↑(List.map ofPTree ts)

@[simp]

theorem HopfAlgebras.RootedTree.branches_bullet :

bullet.branches = 0

def HopfAlgebras.RootedForest.empty :

The empty rooted forest.

Equations

HopfAlgebras.RootedForest.empty = 0

Instances For

def HopfAlgebras.RootedForest.singleton (τ : RootedTree) :

The one-tree forest.

Equations

HopfAlgebras.RootedForest.singleton τ = {τ}

Instances For

def HopfAlgebras.RootedForest.order (φ : RootedForest) :

The total number of vertices in a rooted forest.

Equations

φ.order = (Multiset.map HopfAlgebras.RootedTree.order φ).sum

Instances For

def HopfAlgebras.RootedForest.IsOfOrder (φ : RootedForest) (n : ℕ) :

Predicate for rooted forests of a fixed order.

Equations

φ.IsOfOrder n = (φ.order = n)

Instances For

def HopfAlgebras.RootedForest.treeFactorial (φ : RootedForest) :

The product of the tree factorials in a rooted forest.

Equations

φ.treeFactorial = (Multiset.map HopfAlgebras.RootedTree.treeFactorial φ).prod

Instances For

noncomputable def HopfAlgebras.RootedForest.graft :

RootedForest → RootedTree

The B_+ operator: graft all roots in a forest onto one new common root.

Equations

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

Instances For

@[simp]

theorem HopfAlgebras.RootedForest.graft_coe (ts : List RootedTree) :

graft ↑ts = RootedTree.ofPTree (PTree.node (List.map Quotient.out ts))

@[simp]

theorem HopfAlgebras.RootedForest.graft_empty :

empty.graft = RootedTree.bullet

@[simp]

theorem HopfAlgebras.RootedForest.graft_zero :

graft 0 = RootedTree.bullet

@[simp]

theorem HopfAlgebras.RootedForest.branches_graft (φ : RootedForest) :

φ.graft.branches = φ

theorem HopfAlgebras.RootedForest.graft_injective :

Function.Injective graft

@[simp]

theorem HopfAlgebras.RootedForest.graft_eq_graft_iff (φ ψ : RootedForest) :

φ.graft = ψ.graft ↔ φ = ψ

@[simp]

theorem HopfAlgebras.RootedForest.order_empty :

empty.order = 0

@[simp]

theorem HopfAlgebras.RootedForest.order_zero :

@[simp]

theorem HopfAlgebras.RootedForest.order_singleton (τ : RootedTree) :

(singleton τ).order = τ.order

theorem HopfAlgebras.RootedForest.singleton_ne_zero (τ : RootedTree) :

singleton τ ≠ 0

@[simp]

theorem HopfAlgebras.RootedForest.order_ofPTree_list (ts : List PTree) :

order ↑(List.map RootedTree.ofPTree ts) = PTree.orderList ts

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_ofPTree_list (ts : List PTree) :

treeFactorial ↑(List.map RootedTree.ofPTree ts) = PTree.treeFactorialList ts

@[simp]

theorem HopfAlgebras.RootedForest.order_add (φ ψ : RootedForest) :

(φ + ψ).order = φ.order + ψ.order

theorem HopfAlgebras.RootedForest.order_coe_cons_pos (τ : RootedTree) (ts : List RootedTree) :

0 < order ↑(τ :: ts)

@[simp]

theorem HopfAlgebras.RootedForest.order_eq_zero_iff (φ : RootedForest) :

φ.order = 0 ↔ φ = 0

theorem HopfAlgebras.RootedForest.order_pos_iff_ne_zero (φ : RootedForest) :

0 < φ.order ↔ φ ≠ 0

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_empty :

empty.treeFactorial = 1

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_zero :

treeFactorial 0 = 1

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_singleton (τ : RootedTree) :

(singleton τ).treeFactorial = τ.treeFactorial

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_add (φ ψ : RootedForest) :

(φ + ψ).treeFactorial = φ.treeFactorial * ψ.treeFactorial

theorem HopfAlgebras.RootedForest.treeFactorial_pos (φ : RootedForest) :

0 < φ.treeFactorial

theorem HopfAlgebras.RootedForest.treeFactorial_ne_zero (φ : RootedForest) :

φ.treeFactorial ≠ 0

@[simp]

theorem HopfAlgebras.RootedForest.order_graft (φ : RootedForest) :

φ.graft.order = 1 + φ.order

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_graft (φ : RootedForest) :

φ.graft.treeFactorial = (1 + φ.order) * φ.treeFactorial

theorem HopfAlgebras.RootedForest.graft_ofPTree_list (ts : List PTree) :

graft ↑(List.map RootedTree.ofPTree ts) = RootedTree.ofPTree (PTree.node ts)

Grafting quotient classes of planar trees agrees with planar PTree.node.

theorem HopfAlgebras.RootedForest.ofPTree_node_eq_of_forestPerm {ts us : List PTree} (h : PTree.ForestPerm ts us) :

RootedTree.ofPTree (PTree.node ts) = RootedTree.ofPTree (PTree.node us)

@[simp]

theorem HopfAlgebras.RootedForest.graft_branches_ofPTree_node (ts : List PTree) :

(RootedTree.ofPTree (PTree.node ts)).branches.graft = RootedTree.ofPTree (PTree.node ts)

@[simp]

theorem HopfAlgebras.RootedForest.graft_branches (τ : RootedTree) :

τ.branches.graft = τ

@[simp]

theorem HopfAlgebras.RootedForest.order_branches (τ : RootedTree) :

1 + τ.branches.order = τ.order

theorem HopfAlgebras.RootedForest.order_branches_lt (τ : RootedTree) :

τ.branches.order < τ.order

theorem HopfAlgebras.RootedForest.branches_eq_zero_of_order_eq_one (τ : RootedTree) (h : τ.order = 1) :

τ.branches = 0

theorem HopfAlgebras.RootedForest.order_eq_one_iff_branches_eq_zero (τ : RootedTree) :

τ.order = 1 ↔ τ.branches = 0

theorem HopfAlgebras.RootedForest.order_eq_one_iff_eq_graft_zero (τ : RootedTree) :

τ.order = 1 ↔ τ = graft 0

theorem HopfAlgebras.RootedForest.treeFactorial_branches (τ : RootedTree) :

τ.order * τ.branches.treeFactorial = τ.treeFactorial

noncomputable def HopfAlgebras.RootedForest.butcherProduct (φ : RootedForest) (τ : RootedTree) :

Graft a rooted forest onto the root of a rooted tree.

Equations

φ.butcherProduct τ = (φ + τ.branches).graft

Instances For

@[simp]

theorem HopfAlgebras.RootedForest.butcherProduct_zero_left (τ : RootedTree) :

butcherProduct 0 τ = τ

@[simp]

theorem HopfAlgebras.RootedForest.butcherProduct_empty_left (τ : RootedTree) :

empty.butcherProduct τ = τ

@[simp]

theorem HopfAlgebras.RootedForest.branches_butcherProduct (φ : RootedForest) (τ : RootedTree) :

(φ.butcherProduct τ).branches = φ + τ.branches

theorem HopfAlgebras.RootedForest.butcherProduct_ofPTree_list (ts : List PTree) (t : PTree) :

RootedTree.ofPTree (PTree.butcherProduct ts t) = butcherProduct (↑(List.map RootedTree.ofPTree ts)) (RootedTree.ofPTree t)

theorem HopfAlgebras.RootedForest.butcherProduct_eq_iff_branches (φ ψ : RootedForest) (τ σ : RootedTree) :

φ.butcherProduct τ = ψ.butcherProduct σ ↔ φ + τ.branches = ψ + σ.branches

theorem HopfAlgebras.RootedForest.butcherProduct_injective_left (τ : RootedTree) :

Function.Injective fun (φ : RootedForest) => φ.butcherProduct τ

theorem HopfAlgebras.RootedForest.butcherProduct_injective_right (φ : RootedForest) :

Function.Injective φ.butcherProduct

@[simp]

theorem HopfAlgebras.RootedForest.butcherProduct_left_eq_left_iff (φ ψ : RootedForest) (τ : RootedTree) :

φ.butcherProduct τ = ψ.butcherProduct τ ↔ φ = ψ

@[simp]

theorem HopfAlgebras.RootedForest.butcherProduct_right_eq_right_iff (φ : RootedForest) (τ σ : RootedTree) :

φ.butcherProduct τ = φ.butcherProduct σ ↔ τ = σ

@[simp]

theorem HopfAlgebras.RootedForest.butcherProduct_assoc (φ ψ : RootedForest) (τ : RootedTree) :

φ.butcherProduct (ψ.butcherProduct τ) = (φ + ψ).butcherProduct τ

@[simp]

theorem HopfAlgebras.RootedForest.order_butcherProduct (φ : RootedForest) (τ : RootedTree) :

(φ.butcherProduct τ).order = φ.order + τ.order

@[simp]

theorem HopfAlgebras.RootedForest.treeFactorial_butcherProduct (φ : RootedForest) (τ : RootedTree) :

(φ.butcherProduct τ).treeFactorial = (φ.order + τ.order) * (φ + τ.branches).treeFactorial