Convolution of Labelled B-Series #
The convolution of labelled B-series coefficient families, expressed through the labelled character convolution, with order-truncation congruence lemmas.
theorem
BSeries.PLTree.evalCoproductTerm_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
(term : HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α)
(hterm : term.1.order + term.2.order ≤ n)
:
theorem
BSeries.PLTree.evalCoproductTerms_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{terms : List (HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α)}
(hterms : ∀ term ∈ terms, term.1.order + term.2.order ≤ n)
:
theorem
BSeries.PLTree.convolutionCoeff_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{t : HopfAlgebras.PLTree α}
(ht : t.order ≤ n)
:
theorem
BSeries.PLTree.convolutionForestCoeff_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{ts : List (HopfAlgebras.PLTree α)}
(hts : HopfAlgebras.PLTree.orderList ts ≤ n)
:
theorem
BSeries.LRootedForest.convolutionCoeff_toCharacter_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{φ : HopfAlgebras.LRootedForest α}
(hφ : φ.order ≤ n)
:
noncomputable def
BSeries.LSeries.planarConvolutionCoeff
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
:
R
Planar labelled convolution coefficient obtained from the cut coproduct.
Equations
Instances For
theorem
BSeries.LSeries.planarConvolutionCoeff_eq_of_cuts_listRelPerm
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
{t u : HopfAlgebras.PLTree α}
(h : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Cut.Perm t.cuts u.cuts)
:
theorem
BSeries.LSeries.planarConvolutionCoeff_eq_of_rootCuts_listRelPerm
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
{t u : HopfAlgebras.PLTree α}
(htu : t.Perm u)
(hroot : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.RootCut.Perm t.rootCuts u.rootCuts)
:
theorem
BSeries.LSeries.planarConvolutionCoeff_perm
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
{t u : HopfAlgebras.PLTree α}
(h : t.Perm u)
:
noncomputable def
BSeries.LSeries.planarConvolutionForestCoeff
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(ts : List (HopfAlgebras.PLTree α))
:
R
Multiplicative extension of planar labelled convolution coefficients.
Equations
Instances For
theorem
BSeries.LSeries.planarConvolutionCoeff_comapEraseLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : Series R)
(t : HopfAlgebras.PLTree α)
:
(comapEraseLabels a).planarConvolutionCoeff (comapEraseLabels b) t = a.planarConvolutionCoeff b t.erase
Pulling unlabelled series back by erasing labels commutes with planar convolution.
theorem
BSeries.LSeries.planarConvolutionForestCoeff_comapEraseLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : Series R)
(ts : List (HopfAlgebras.PLTree α))
:
Pulling unlabelled series back by erasing labels commutes with planar forest convolution.
theorem
BSeries.LSeries.planarConvolutionCoeff_comapConstLabel
{α : Type u}
{R : Type v}
[CommSemiring R]
(x : α)
(a b : LSeries α R)
(t : HopfAlgebras.PTree)
:
(comapConstLabel x a).planarConvolutionCoeff (comapConstLabel x b) t = a.planarConvolutionCoeff b (HopfAlgebras.PLTree.constLabel x t)
theorem
BSeries.LSeries.planarConvolutionForestCoeff_comapConstLabel
{α : Type u}
{R : Type v}
[CommSemiring R]
(x : α)
(a b : LSeries α R)
(ts : List HopfAlgebras.PTree)
:
(comapConstLabel x a).planarConvolutionForestCoeff (comapConstLabel x b) ts = a.planarConvolutionForestCoeff b (List.map (HopfAlgebras.PLTree.constLabel x) ts)
theorem
BSeries.LSeries.LabelInvariant.planarConvolutionCoeff_eq
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
{a b : LSeries α R}
(ha : a.LabelInvariant)
(hb : b.LabelInvariant)
{t u : HopfAlgebras.PLTree α}
(htu : t.erase = u.erase)
:
Planar convolution of label-invariant series depends only on the erased tree.
theorem
BSeries.LSeries.LabelInvariant.planarConvolutionForestCoeff_eq
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
{a b : LSeries α R}
(ha : a.LabelInvariant)
(hb : b.LabelInvariant)
{ts us : List (HopfAlgebras.PLTree α)}
(hts : List.map HopfAlgebras.PLTree.erase ts = List.map HopfAlgebras.PLTree.erase us)
:
Planar forest convolution of label-invariant series depends only on erased forests.
noncomputable def
BSeries.LSeries.forestConvolutionCoeff
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
R
Convolution coefficient on a non-planar labelled rooted forest.
Equations
Instances For
@[simp]
theorem
BSeries.LSeries.forestConvolutionCoeff_zero
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.forestConvolutionCoeff_empty
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.forestConvolutionCoeff_singleton
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(τ : HopfAlgebras.LRootedTree α)
:
theorem
BSeries.LSeries.forestConvolutionCoeff_singleton_ofPLTree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
:
@[simp]
theorem
BSeries.LSeries.forestConvolutionCoeff_add
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(φ ψ : HopfAlgebras.LRootedForest α)
:
theorem
BSeries.LSeries.forestConvolutionCoeff_comapEraseLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : Series R)
(φ : HopfAlgebras.LRootedForest α)
:
(comapEraseLabels a).forestConvolutionCoeff (comapEraseLabels b) φ = a.forestConvolutionCoeff b φ.erase
theorem
BSeries.LSeries.forestConvolutionCoeff_comapMapLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
{β : Type w}
(f : α → β)
(a b : LSeries β R)
(φ : HopfAlgebras.LRootedForest α)
:
(comapMapLabels f a).forestConvolutionCoeff (comapMapLabels f b) φ = a.forestConvolutionCoeff b (HopfAlgebras.LRootedForest.mapLabels f φ)
theorem
BSeries.LSeries.forestConvolutionCoeff_comapConstLabel
{α : Type u}
{R : Type v}
[CommSemiring R]
(x : α)
(a b : LSeries α R)
(φ : HopfAlgebras.RootedForest)
:
(comapConstLabel x a).forestConvolutionCoeff (comapConstLabel x b) φ = a.forestConvolutionCoeff b (HopfAlgebras.LRootedForest.constLabel x φ)
theorem
BSeries.LSeries.planarConvolutionCoeff_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{t : HopfAlgebras.PLTree α}
(ht : t.order ≤ n)
:
theorem
BSeries.LSeries.planarConvolutionForestCoeff_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{ts : List (HopfAlgebras.PLTree α)}
(hts : HopfAlgebras.PLTree.orderList ts ≤ n)
:
theorem
BSeries.LSeries.forestConvolutionCoeff_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{φ : HopfAlgebras.LRootedForest α}
(hφ : φ.order ≤ n)
:
theorem
BSeries.LSeries.forestConvolutionCoeff_unit_right
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
theorem
BSeries.LSeries.forestConvolutionCoeff_unit_left
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
noncomputable def
BSeries.LSeries.convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
LSeries α R
Convolution product of two labelled B-series coefficient families.
Equations
Instances For
@[simp]
theorem
BSeries.LSeries.convolution_empty
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.convolution_tree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(τ : HopfAlgebras.LRootedTree α)
:
(a.convolution b).coeff (LTreeIndex.tree τ) = a.forestConvolutionCoeff b (HopfAlgebras.LRootedForest.singleton τ)
theorem
BSeries.LSeries.convolution_tree_eq_treeConvolutionCoeff
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(τ : HopfAlgebras.LRootedTree α)
:
theorem
BSeries.LSeries.convolution_tree_comapEraseLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : Series R)
(τ : HopfAlgebras.LRootedTree α)
:
((comapEraseLabels a).convolution (comapEraseLabels b)).coeff (LTreeIndex.tree τ) = (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ.erase)
theorem
BSeries.LSeries.convolution_comapEraseLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : Series R)
:
theorem
BSeries.LSeries.convolution_tree_comapMapLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
{β : Type w}
(f : α → β)
(a b : LSeries β R)
(τ : HopfAlgebras.LRootedTree α)
:
((comapMapLabels f a).convolution (comapMapLabels f b)).coeff (LTreeIndex.tree τ) = (a.convolution b).coeff (LTreeIndex.tree (HopfAlgebras.LRootedTree.map f τ))
theorem
BSeries.LSeries.convolution_comapMapLabels
{α : Type u}
{R : Type v}
[CommSemiring R]
{β : Type w}
(f : α → β)
(a b : LSeries β R)
:
theorem
BSeries.LSeries.convolution_tree_comapConstLabel
{α : Type u}
{R : Type v}
[CommSemiring R]
(x : α)
(a b : LSeries α R)
(τ : HopfAlgebras.RootedTree)
:
((comapConstLabel x a).convolution (comapConstLabel x b)).coeff (HopfAlgebras.TreeIndex.tree τ) = (a.convolution b).coeff (LTreeIndex.tree (HopfAlgebras.LRootedTree.constLabel x τ))
theorem
BSeries.LSeries.convolution_comapConstLabel
{α : Type u}
{R : Type v}
[CommSemiring R]
(x : α)
(a b : LSeries α R)
:
theorem
BSeries.LSeries.LabelInvariant.convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
{a b : LSeries α R}
(ha : a.LabelInvariant)
(hb : b.LabelInvariant)
:
(a.convolution b).LabelInvariant
theorem
BSeries.LSeries.labelInvariantEquiv_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
(a b : Series R)
:
labelInvariantEquiv (a.convolution b) = ⟨(↑(labelInvariantEquiv a)).convolution ↑(labelInvariantEquiv b), ⋯⟩
theorem
BSeries.LSeries.labelInvariantUnitEquiv_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
(a b : { a : Series R // a.HasUnitConstant })
:
labelInvariantUnitEquiv ⟨(↑a).convolution ↑b, ⋯⟩ = ⟨(↑(labelInvariantUnitEquiv a)).convolution ↑(labelInvariantUnitEquiv b), ⋯⟩
theorem
BSeries.LSeries.labelInvariantEquiv_symm_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
(a b : { a : LSeries α R // a.LabelInvariant })
:
labelInvariantEquiv.symm ⟨(↑a).convolution ↑b, ⋯⟩ = (labelInvariantEquiv.symm a).convolution (labelInvariantEquiv.symm b)
theorem
BSeries.LSeries.labelInvariantUnitEquiv_symm_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
(a b : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant })
:
labelInvariantUnitEquiv.symm ⟨(↑a).convolution ↑b, ⋯⟩ = ⟨(↑(labelInvariantUnitEquiv.symm a)).convolution ↑(labelInvariantUnitEquiv.symm b), ⋯⟩
theorem
BSeries.LSeries.convolution_tree_ofPLTree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
:
(a.convolution b).coeff (LTreeIndex.tree (HopfAlgebras.LRootedTree.ofPLTree t)) = a.planarConvolutionCoeff b t
theorem
BSeries.LSeries.convolution_hasUnitConstant
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
(a.convolution b).HasUnitConstant
theorem
BSeries.LSeries.forestCoeff_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
theorem
BSeries.LSeries.forestCoeff_convolution_singleton_tree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(τ : HopfAlgebras.LRootedTree α)
:
theorem
BSeries.LSeries.forestCoeff_convolution_singleton_ofPLTree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
:
theorem
BSeries.LSeries.forestCoeff_convolution_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{φ : HopfAlgebras.LRootedForest α}
(hφ : φ.order ≤ n)
:
theorem
BSeries.LSeries.forestCoeff_convolution_congr_left_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
{φ : HopfAlgebras.LRootedForest α}
:
φ.order ≤ n → (a.convolution b).forestCoeff φ = (a'.convolution b).forestCoeff φ
theorem
BSeries.LSeries.forestCoeff_convolution_congr_right_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b b' : LSeries α R}
{n : ℕ}
(hb : b.AgreeUpToOrder b' n)
{φ : HopfAlgebras.LRootedForest α}
:
φ.order ≤ n → (a.convolution b).forestCoeff φ = (a.convolution b').forestCoeff φ
@[simp]
theorem
BSeries.LSeries.forestCoeff_convolution_unit_right
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
@[simp]
theorem
BSeries.LSeries.forestCoeff_convolution_unit_left
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
@[simp]
theorem
BSeries.LSeries.toCharacter_convolution_ofForest
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(φ : HopfAlgebras.LRootedForest α)
:
theorem
BSeries.LSeries.toCharacter_convolution_ofForest_singleton_tree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(τ : HopfAlgebras.LRootedTree α)
:
theorem
BSeries.LSeries.toCharacter_convolution_ofForest_singleton_ofPLTree
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
:
@[simp]
theorem
BSeries.LSeries.toCharacter_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.toCharacter_convolution_unit_right
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.toCharacter_convolution_unit_left
{α : Type u}
{R : Type v}
[CommSemiring R]
(a : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.ofCharacter_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(χ ψ : HopfAlgebras.LForestAlgebra.Character α R)
:
theorem
BSeries.LSeries.ofCharacter_convolution_toCharacter
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.characterEquiv_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : { a : LSeries α R // a.HasUnitConstant })
:
theorem
BSeries.LSeries.labelInvariantCharacterEquiv_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
(a b : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant })
:
labelInvariantCharacterEquiv ⟨(↑a).convolution ↑b, ⋯⟩ = ⟨(↑(labelInvariantCharacterEquiv a)).convolution ↑(labelInvariantCharacterEquiv b), ⋯⟩
theorem
BSeries.LSeries.characterEquiv_symm_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
(χ ψ : HopfAlgebras.LForestAlgebra.Character α R)
:
↑(characterEquiv.symm (χ.convolution ψ)) = (↑(characterEquiv.symm χ)).convolution ↑(characterEquiv.symm ψ)
theorem
BSeries.LSeries.eq_convolution_of_toCharacter_eq
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b c : LSeries α R}
(hc : c.HasUnitConstant)
(h : c.toCharacter = a.toCharacter.convolution b.toCharacter)
:
theorem
BSeries.LSeries.convolution_assoc_of_character_assoc
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b c : LSeries α R}
(hassoc :
(a.toCharacter.convolution b.toCharacter).convolution c.toCharacter = a.toCharacter.convolution (b.toCharacter.convolution c.toCharacter))
:
theorem
BSeries.LSeries.convolution_assoc_of_coproduct_eq
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc :
∀ (x : HopfAlgebras.LForestAlgebra α R),
(HopfAlgebras.LForestAlgebra.coproductLeft α R) x = (HopfAlgebras.LForestAlgebra.coproductRight α R) x)
(a b c : LSeries α R)
:
theorem
BSeries.LSeries.convolution_assoc_of_coproductLeft_eq_coproductRight
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc : HopfAlgebras.LForestAlgebra.coproductLeft α R = HopfAlgebras.LForestAlgebra.coproductRight α R)
(a b c : LSeries α R)
:
theorem
BSeries.LSeries.convolution_assoc_of_nestedCoproductTerms
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc :
∀ (t : HopfAlgebras.PLTree α),
HopfAlgebras.LForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = HopfAlgebras.LForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms)
(a b c : LSeries α R)
:
theorem
BSeries.LSeries.convolution_assoc_of_nestedCoproductTerms_perm
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc : ∀ (t : HopfAlgebras.PLTree α), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms)
(a b c : LSeries α R)
:
theorem
BSeries.LSeries.convolution_assoc
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b c : LSeries α R)
:
theorem
BSeries.LSeries.agreeUpToOrder_convolution_assoc_of_character_assoc
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b c : LSeries α R}
(hassoc :
(a.toCharacter.convolution b.toCharacter).convolution c.toCharacter = a.toCharacter.convolution (b.toCharacter.convolution c.toCharacter))
(n : ℕ)
:
((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_assoc_of_coproduct_eq
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc :
∀ (x : HopfAlgebras.LForestAlgebra α R),
(HopfAlgebras.LForestAlgebra.coproductLeft α R) x = (HopfAlgebras.LForestAlgebra.coproductRight α R) x)
(a b c : LSeries α R)
(n : ℕ)
:
((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_assoc_of_coproductLeft_eq_coproductRight
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc : HopfAlgebras.LForestAlgebra.coproductLeft α R = HopfAlgebras.LForestAlgebra.coproductRight α R)
(a b c : LSeries α R)
(n : ℕ)
:
((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_assoc_of_nestedCoproductTerms_perm
{α : Type u}
{R : Type v}
[CommSemiring R]
(hcoassoc : ∀ (t : HopfAlgebras.PLTree α), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms)
(a b c : LSeries α R)
(n : ℕ)
:
((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_assoc
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b c : LSeries α R)
(n : ℕ)
:
((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n
theorem
BSeries.LSeries.convolution_tree_congr_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
{τ : HopfAlgebras.LRootedTree α}
(hτ : τ.order ≤ n)
:
theorem
BSeries.LSeries.convolution_tree_congr_left_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
{τ : HopfAlgebras.LRootedTree α}
:
τ.order ≤ n → (a.convolution b).coeff (LTreeIndex.tree τ) = (a'.convolution b).coeff (LTreeIndex.tree τ)
theorem
BSeries.LSeries.convolution_tree_congr_right_of_agree
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b b' : LSeries α R}
{n : ℕ}
(hb : b.AgreeUpToOrder b' n)
{τ : HopfAlgebras.LRootedTree α}
:
τ.order ≤ n → (a.convolution b).coeff (LTreeIndex.tree τ) = (a.convolution b').coeff (LTreeIndex.tree τ)
theorem
BSeries.LSeries.agreeUpToOrder_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
:
(a.convolution b).AgreeUpToOrder (a'.convolution b') n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_left
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
:
(a.convolution b).AgreeUpToOrder (a'.convolution b) n
theorem
BSeries.LSeries.agreeUpToOrder_convolution_right
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b b' : LSeries α R}
{n : ℕ}
(hb : b.AgreeUpToOrder b' n)
:
(a.convolution b).AgreeUpToOrder (a.convolution b') n
theorem
BSeries.LSeries.convolution_eq_of_agreeUpToOrder_all
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
:
theorem
BSeries.LSeries.convolution_left_eq_of_agreeUpToOrder_all
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
:
theorem
BSeries.LSeries.convolution_right_eq_of_agreeUpToOrder_all
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b b' : LSeries α R}
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
:
theorem
BSeries.LSeries.agreeUpToOrder_all_convolution
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b b' : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
(n : ℕ)
:
(a.convolution b).AgreeUpToOrder (a'.convolution b') n
theorem
BSeries.LSeries.agreeUpToOrder_all_convolution_left
{α : Type u}
{R : Type v}
[CommSemiring R]
{a a' b : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
(n : ℕ)
:
(a.convolution b).AgreeUpToOrder (a'.convolution b) n
theorem
BSeries.LSeries.agreeUpToOrder_all_convolution_right
{α : Type u}
{R : Type v}
[CommSemiring R]
{a b b' : LSeries α R}
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
(n : ℕ)
:
(a.convolution b).AgreeUpToOrder (a.convolution b') n
theorem
BSeries.LSeries.convolution_unit_right
{α : Type u}
{R : Type v}
[CommSemiring R]
{a : LSeries α R}
(ha : a.HasUnitConstant)
:
theorem
BSeries.LSeries.convolution_unit_left
{α : Type u}
{R : Type v}
[CommSemiring R]
{a : LSeries α R}
(ha : a.HasUnitConstant)
:
@[implicit_reducible]
noncomputable instance
BSeries.LSeries.instUnitConstantMonoid
{α : Type u}
{R : Type v}
[CommSemiring R]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- BSeries.LSeries.characterMulEquiv = { toEquiv := BSeries.LSeries.characterEquiv, map_mul' := ⋯ }
Instances For
@[implicit_reducible]
noncomputable instance
BSeries.LSeries.instLabelInvariantUnitConstantMonoid
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
:
Monoid { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
BSeries.LSeries.labelInvariantUnitMulEquiv
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
:
{ a : Series R // a.HasUnitConstant } ≃* { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }
Equations
- BSeries.LSeries.labelInvariantUnitMulEquiv = { toEquiv := BSeries.LSeries.labelInvariantUnitEquiv, map_mul' := ⋯ }
Instances For
noncomputable def
BSeries.LSeries.labelInvariantCharacterMulEquiv
{α : Type u}
{R : Type v}
[CommSemiring R]
[Nonempty α]
:
{ a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant } ≃* { χ : HopfAlgebras.LForestAlgebra.Character α R // χ.LabelInvariant }
Equations
- BSeries.LSeries.labelInvariantCharacterMulEquiv = { toEquiv := BSeries.LSeries.labelInvariantCharacterEquiv, map_mul' := ⋯ }
Instances For
@[simp]
theorem
BSeries.LSeries.planarConvolutionForestCoeff_nil
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
:
@[simp]
theorem
BSeries.LSeries.planarConvolutionForestCoeff_cons
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
(t : HopfAlgebras.PLTree α)
(ts : List (HopfAlgebras.PLTree α))
:
a.planarConvolutionForestCoeff b (t :: ts) = a.planarConvolutionCoeff b t * a.planarConvolutionForestCoeff b ts
theorem
BSeries.LSeries.planarConvolutionForestCoeff_perm
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
{ts us : List (HopfAlgebras.PLTree α)}
(h : ts.Perm us)
:
theorem
BSeries.LSeries.planarConvolutionForestCoeff_forall₂_perm
{α : Type u}
{R : Type v}
[CommSemiring R]
(a b : LSeries α R)
{ts us : List (HopfAlgebras.PLTree α)}
:
List.Forall₂ HopfAlgebras.PLTree.Perm ts us → a.planarConvolutionForestCoeff b ts = a.planarConvolutionForestCoeff b us
theorem
BSeries.LSeries.convolution_hasOrder_zero
{α : Type u}
{R : Type v}
[Field R]
(a b : LSeries α R)
:
(a.convolution b).HasOrder 0
theorem
BSeries.LSeries.convolution_hasOrder_all_congr
{α : Type u}
{R : Type v}
[Field R]
{a a' b b' : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
:
theorem
BSeries.LSeries.convolution_hasOrder_congr
{α : Type u}
{R : Type v}
[Field R]
{a a' b b' : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
(hb : b.AgreeUpToOrder b' n)
:
theorem
BSeries.LSeries.convolution_hasOrder_all_congr_left
{α : Type u}
{R : Type v}
[Field R]
{a a' b : LSeries α R}
(ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n)
:
theorem
BSeries.LSeries.convolution_hasOrder_congr_left
{α : Type u}
{R : Type v}
[Field R]
{a a' b : LSeries α R}
{n : ℕ}
(ha : a.AgreeUpToOrder a' n)
:
theorem
BSeries.LSeries.convolution_hasOrder_all_congr_right
{α : Type u}
{R : Type v}
[Field R]
{a b b' : LSeries α R}
(hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n)
:
theorem
BSeries.LSeries.convolution_hasOrder_congr_right
{α : Type u}
{R : Type v}
[Field R]
{a b b' : LSeries α R}
{n : ℕ}
(hb : b.AgreeUpToOrder b' n)
: