Convolution of B-Series

The Butcher-group convolution of B-series coefficient families, expressed through the character convolution of Hopf/CharacterConvolution.lean, with the congruence lemmas for order-truncated agreement.

theorem BSeries.PTree.evalCoproductTerm_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) (hterm : term.1.order + term.2.order ≤ n) : HopfAlgebras.PTree.evalCoproductTerm a.toCharacter b.toCharacter term = HopfAlgebras.PTree.evalCoproductTerm a'.toCharacter b'.toCharacter term

theorem BSeries.PTree.evalCoproductTerms_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {terms : List (HopfAlgebras.RootedForest × HopfAlgebras.RootedForest)} (hterms : ∀ term ∈ terms, term.1.order + term.2.order ≤ n) : HopfAlgebras.PTree.evalCoproductTerms a.toCharacter b.toCharacter terms = HopfAlgebras.PTree.evalCoproductTerms a'.toCharacter b'.toCharacter terms

theorem BSeries.PTree.convolutionCoeff_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {t : HopfAlgebras.PTree} (ht : t.order ≤ n) : HopfAlgebras.PTree.convolutionCoeff a.toCharacter b.toCharacter t = HopfAlgebras.PTree.convolutionCoeff a'.toCharacter b'.toCharacter t

theorem BSeries.PTree.convolutionForestCoeff_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {ts : List HopfAlgebras.PTree} (hts : HopfAlgebras.PTree.orderList ts ≤ n) : HopfAlgebras.PTree.convolutionForestCoeff a.toCharacter b.toCharacter ts = HopfAlgebras.PTree.convolutionForestCoeff a'.toCharacter b'.toCharacter ts

theorem BSeries.RootedForest.convolutionCoeff_toCharacter_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : HopfAlgebras.RootedForest.convolutionCoeff a.toCharacter b.toCharacter φ = HopfAlgebras.RootedForest.convolutionCoeff a'.toCharacter b'.toCharacter φ

noncomputable def BSeries.Series.planarConvolutionCoeff {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) : R

Planar convolution coefficient obtained from the cut coproduct.

Equations

• a.planarConvolutionCoeff b t = HopfAlgebras.PTree.convolutionCoeff a.toCharacter b.toCharacter t

noncomputable def BSeries.Series.planarConvolutionForestCoeff {R : Type u} [CommSemiring R] (a b : Series R) (ts : List HopfAlgebras.PTree) : R

Multiplicative extension of planar convolution coefficients to planar forests.

Equations

• a.planarConvolutionForestCoeff b ts = HopfAlgebras.PTree.convolutionForestCoeff a.toCharacter b.toCharacter ts

theorem BSeries.Series.planarConvolutionCoeff_eq_of_cuts_listRelPerm {R : Type u} [CommSemiring R] (a b : Series R) {t u : HopfAlgebras.PTree} (h : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Cut.Perm t.cuts u.cuts) : a.planarConvolutionCoeff b t = a.planarConvolutionCoeff b u

theorem BSeries.Series.planarConvolutionCoeff_eq_of_rootCuts_listRelPerm {R : Type u} [CommSemiring R] (a b : Series R) {t u : HopfAlgebras.PTree} (htu : t.Perm u) (hroot : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.RootCut.Perm t.rootCuts u.rootCuts) : a.planarConvolutionCoeff b t = a.planarConvolutionCoeff b u

theorem BSeries.Series.planarConvolutionCoeff_perm {R : Type u} [CommSemiring R] (a b : Series R) {t u : HopfAlgebras.PTree} (h : t.Perm u) : a.planarConvolutionCoeff b t = a.planarConvolutionCoeff b u

noncomputable def BSeries.Series.forestConvolutionCoeff {R : Type u} [CommSemiring R] (a b : Series R) (φ : HopfAlgebras.RootedForest) : R

Convolution coefficient on a non-planar rooted forest.

Equations

• a.forestConvolutionCoeff b φ = HopfAlgebras.RootedForest.convolutionCoeff a.toCharacter b.toCharacter φ

@[simp]

theorem BSeries.Series.forestConvolutionCoeff_zero {R : Type u} [CommSemiring R] (a b : Series R) : a.forestConvolutionCoeff b 0 = 1

@[simp]

theorem BSeries.Series.forestConvolutionCoeff_empty {R : Type u} [CommSemiring R] (a b : Series R) : a.forestConvolutionCoeff b HopfAlgebras.RootedForest.empty = 1

@[simp]

theorem BSeries.Series.forestConvolutionCoeff_singleton {R : Type u} [CommSemiring R] (a b : Series R) (τ : HopfAlgebras.RootedTree) : a.forestConvolutionCoeff b (HopfAlgebras.RootedForest.singleton τ) = a.planarConvolutionCoeff b (Quotient.out τ)

theorem BSeries.Series.forestConvolutionCoeff_singleton_ofPTree {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) : a.forestConvolutionCoeff b (HopfAlgebras.RootedForest.singleton (HopfAlgebras.RootedTree.ofPTree t)) = a.planarConvolutionCoeff b t

@[simp]

theorem BSeries.Series.forestConvolutionCoeff_add {R : Type u} [CommSemiring R] (a b : Series R) (φ ψ : HopfAlgebras.RootedForest) : a.forestConvolutionCoeff b (φ + ψ) = a.forestConvolutionCoeff b φ * a.forestConvolutionCoeff b ψ

theorem BSeries.Series.planarConvolutionCoeff_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {t : HopfAlgebras.PTree} (ht : t.order ≤ n) : a.planarConvolutionCoeff b t = a'.planarConvolutionCoeff b' t

theorem BSeries.Series.planarConvolutionForestCoeff_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {ts : List HopfAlgebras.PTree} (hts : HopfAlgebras.PTree.orderList ts ≤ n) : a.planarConvolutionForestCoeff b ts = a'.planarConvolutionForestCoeff b' ts

theorem BSeries.Series.forestConvolutionCoeff_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : a.forestConvolutionCoeff b φ = a'.forestConvolutionCoeff b' φ

theorem BSeries.Series.forestConvolutionCoeff_unit_right {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : a.forestConvolutionCoeff (unit R) φ = a.forestCoeff φ

theorem BSeries.Series.forestConvolutionCoeff_unit_left {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : (unit R).forestConvolutionCoeff a φ = a.forestCoeff φ

noncomputable def BSeries.Series.convolution {R : Type u} [CommSemiring R] (a b : Series R) : Series R

Convolution product of two B-series coefficient families.

Equations

• a.convolution b HopfAlgebras.TreeIndex.empty = 1
• a.convolution b (HopfAlgebras.TreeIndex.tree τ) = a.forestConvolutionCoeff b (HopfAlgebras.RootedForest.singleton τ)

@[simp]

theorem BSeries.Series.convolution_empty {R : Type u} [CommSemiring R] (a b : Series R) : (a.convolution b).coeff HopfAlgebras.TreeIndex.empty = 1

@[simp]

theorem BSeries.Series.convolution_tree {R : Type u} [CommSemiring R] (a b : Series R) (τ : HopfAlgebras.RootedTree) : (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ) = a.forestConvolutionCoeff b (HopfAlgebras.RootedForest.singleton τ)

theorem BSeries.Series.convolution_tree_eq_treeConvolutionCoeff {R : Type u} [CommSemiring R] (a b : Series R) (τ : HopfAlgebras.RootedTree) : (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ) = HopfAlgebras.RootedTree.convolutionCoeff a.toCharacter b.toCharacter τ

theorem BSeries.Series.convolution_tree_ofPTree {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) : (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree (HopfAlgebras.RootedTree.ofPTree t)) = a.planarConvolutionCoeff b t

theorem BSeries.Series.convolution_hasUnitConstant {R : Type u} [CommSemiring R] (a b : Series R) : (a.convolution b).HasUnitConstant

theorem BSeries.Series.forestCoeff_convolution {R : Type u} [CommSemiring R] (a b : Series R) (φ : HopfAlgebras.RootedForest) : (a.convolution b).forestCoeff φ = a.forestConvolutionCoeff b φ

theorem BSeries.Series.forestCoeff_convolution_singleton_tree {R : Type u} [CommSemiring R] (a b : Series R) (τ : HopfAlgebras.RootedTree) : (a.convolution b).forestCoeff (HopfAlgebras.RootedForest.singleton τ) = HopfAlgebras.RootedTree.convolutionCoeff a.toCharacter b.toCharacter τ

theorem BSeries.Series.forestCoeff_convolution_singleton_ofPTree {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) : (a.convolution b).forestCoeff (HopfAlgebras.RootedForest.singleton (HopfAlgebras.RootedTree.ofPTree t)) = a.planarConvolutionCoeff b t

theorem BSeries.Series.forestCoeff_convolution_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : (a.convolution b).forestCoeff φ = (a'.convolution b').forestCoeff φ

theorem BSeries.Series.forestCoeff_convolution_congr_left_of_agree {R : Type u} [CommSemiring R] {a a' b : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) {φ : HopfAlgebras.RootedForest} : φ.order ≤ n → (a.convolution b).forestCoeff φ = (a'.convolution b).forestCoeff φ

theorem BSeries.Series.forestCoeff_convolution_congr_right_of_agree {R : Type u} [CommSemiring R] {a b b' : Series R} {n : ℕ} (hb : b.AgreeUpToOrder b' n) {φ : HopfAlgebras.RootedForest} : φ.order ≤ n → (a.convolution b).forestCoeff φ = (a.convolution b').forestCoeff φ

@[simp]

theorem BSeries.Series.forestCoeff_convolution_unit_right {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : (a.convolution (unit R)).forestCoeff φ = a.forestCoeff φ

@[simp]

theorem BSeries.Series.forestCoeff_convolution_unit_left {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : ((unit R).convolution a).forestCoeff φ = a.forestCoeff φ

@[simp]

theorem BSeries.Series.toCharacter_convolution_ofForest {R : Type u} [CommSemiring R] (a b : Series R) (φ : HopfAlgebras.RootedForest) : (a.convolution b).toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = a.forestConvolutionCoeff b φ

theorem BSeries.Series.toCharacter_convolution_ofForest_singleton_tree {R : Type u} [CommSemiring R] (a b : Series R) (τ : HopfAlgebras.RootedTree) : (a.convolution b).toCharacter (HopfAlgebras.ForestAlgebra.ofForest (HopfAlgebras.RootedForest.singleton τ)) = HopfAlgebras.RootedTree.convolutionCoeff a.toCharacter b.toCharacter τ

theorem BSeries.Series.toCharacter_convolution_ofForest_singleton_ofPTree {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) : (a.convolution b).toCharacter (HopfAlgebras.ForestAlgebra.ofForest (HopfAlgebras.RootedForest.singleton (HopfAlgebras.RootedTree.ofPTree t))) = a.planarConvolutionCoeff b t

@[simp]

theorem BSeries.Series.toCharacter_convolution {R : Type u} [CommSemiring R] (a b : Series R) : (a.convolution b).toCharacter = a.toCharacter.convolution b.toCharacter

@[simp]

theorem BSeries.Series.toCharacter_convolution_unit_right {R : Type u} [CommSemiring R] (a : Series R) : (a.convolution (unit R)).toCharacter = a.toCharacter

@[simp]

theorem BSeries.Series.toCharacter_convolution_unit_left {R : Type u} [CommSemiring R] (a : Series R) : ((unit R).convolution a).toCharacter = a.toCharacter

@[simp]

theorem BSeries.Series.ofCharacter_character_unit {R : Type u} [CommSemiring R] : ofCharacter (HopfAlgebras.ForestAlgebra.Character.unit R) = unit R

theorem BSeries.Series.ofCharacter_convolution {R : Type u} [CommSemiring R] (χ ψ : HopfAlgebras.ForestAlgebra.Character R) : ofCharacter (χ.convolution ψ) = (ofCharacter χ).convolution (ofCharacter ψ)

theorem BSeries.Series.ofCharacter_convolution_toCharacter {R : Type u} [CommSemiring R] (a b : Series R) : ofCharacter (a.toCharacter.convolution b.toCharacter) = a.convolution b

@[simp]

theorem BSeries.Series.characterEquiv_unit {R : Type u} [CommSemiring R] : characterEquiv ⟨unit R, ⋯⟩ = HopfAlgebras.ForestAlgebra.Character.unit R

theorem BSeries.Series.characterEquiv_convolution {R : Type u} [CommSemiring R] (a b : { a : Series R // a.HasUnitConstant }) : characterEquiv ⟨(↑a).convolution ↑b, ⋯⟩ = (characterEquiv a).convolution (characterEquiv b)

theorem BSeries.Series.characterEquiv_symm_convolution {R : Type u} [CommSemiring R] (χ ψ : HopfAlgebras.ForestAlgebra.Character R) : ↑(characterEquiv.symm (χ.convolution ψ)) = (↑(characterEquiv.symm χ)).convolution ↑(characterEquiv.symm ψ)

theorem BSeries.Series.eq_convolution_of_toCharacter_eq {R : Type u} [CommSemiring R] {a b c : Series R} (hc : c.HasUnitConstant) (h : c.toCharacter = a.toCharacter.convolution b.toCharacter) : c = a.convolution b

theorem BSeries.Series.convolution_assoc_of_character_assoc {R : Type u} [CommSemiring R] {a b c : Series R} (hassoc : (a.toCharacter.convolution b.toCharacter).convolution c.toCharacter = a.toCharacter.convolution (b.toCharacter.convolution c.toCharacter)) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.convolution_assoc_of_coproduct_eq {R : Type u} [CommSemiring R] (hcoassoc : ∀ (x : HopfAlgebras.ForestAlgebra R), (HopfAlgebras.ForestAlgebra.coproductLeft R) x = (HopfAlgebras.ForestAlgebra.coproductRight R) x) (a b c : Series R) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.convolution_assoc_of_coproductLeft_eq_coproductRight {R : Type u} [CommSemiring R] (hcoassoc : HopfAlgebras.ForestAlgebra.coproductLeft R = HopfAlgebras.ForestAlgebra.coproductRight R) (a b c : Series R) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.convolution_assoc_of_nestedCoproductTerms {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : HopfAlgebras.PTree), HopfAlgebras.ForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = HopfAlgebras.ForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms) (a b c : Series R) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.convolution_assoc_of_nestedCoproductTerms_perm {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : HopfAlgebras.PTree), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) (a b c : Series R) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.convolution_assoc {R : Type u} [CommSemiring R] (a b c : Series R) : (a.convolution b).convolution c = a.convolution (b.convolution c)

theorem BSeries.Series.agreeUpToOrder_convolution_assoc_of_character_assoc {R : Type u} [CommSemiring R] {a b c : Series 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.Series.agreeUpToOrder_convolution_assoc_of_coproduct_eq {R : Type u} [CommSemiring R] (hcoassoc : ∀ (x : HopfAlgebras.ForestAlgebra R), (HopfAlgebras.ForestAlgebra.coproductLeft R) x = (HopfAlgebras.ForestAlgebra.coproductRight R) x) (a b c : Series R) (n : ℕ) : ((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n

theorem BSeries.Series.agreeUpToOrder_convolution_assoc_of_coproductLeft_eq_coproductRight {R : Type u} [CommSemiring R] (hcoassoc : HopfAlgebras.ForestAlgebra.coproductLeft R = HopfAlgebras.ForestAlgebra.coproductRight R) (a b c : Series R) (n : ℕ) : ((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n

theorem BSeries.Series.agreeUpToOrder_convolution_assoc_of_nestedCoproductTerms_perm {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : HopfAlgebras.PTree), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) (a b c : Series R) (n : ℕ) : ((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n

theorem BSeries.Series.agreeUpToOrder_convolution_assoc {R : Type u} [CommSemiring R] (a b c : Series R) (n : ℕ) : ((a.convolution b).convolution c).AgreeUpToOrder (a.convolution (b.convolution c)) n

theorem BSeries.Series.convolution_tree_congr_of_agree {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ) = (a'.convolution b').coeff (HopfAlgebras.TreeIndex.tree τ)

theorem BSeries.Series.convolution_tree_congr_left_of_agree {R : Type u} [CommSemiring R] {a a' b : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) {τ : HopfAlgebras.RootedTree} : τ.order ≤ n → (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ) = (a'.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ)

theorem BSeries.Series.convolution_tree_congr_right_of_agree {R : Type u} [CommSemiring R] {a b b' : Series R} {n : ℕ} (hb : b.AgreeUpToOrder b' n) {τ : HopfAlgebras.RootedTree} : τ.order ≤ n → (a.convolution b).coeff (HopfAlgebras.TreeIndex.tree τ) = (a.convolution b').coeff (HopfAlgebras.TreeIndex.tree τ)

theorem BSeries.Series.agreeUpToOrder_convolution {R : Type u} [CommSemiring R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) : (a.convolution b).AgreeUpToOrder (a'.convolution b') n

theorem BSeries.Series.agreeUpToOrder_convolution_left {R : Type u} [CommSemiring R] {a a' b : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) : (a.convolution b).AgreeUpToOrder (a'.convolution b) n

theorem BSeries.Series.agreeUpToOrder_convolution_right {R : Type u} [CommSemiring R] {a b b' : Series R} {n : ℕ} (hb : b.AgreeUpToOrder b' n) : (a.convolution b).AgreeUpToOrder (a.convolution b') n

theorem BSeries.Series.convolution_eq_of_agreeUpToOrder_all {R : Type u} [CommSemiring R] {a a' b b' : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) : a.convolution b = a'.convolution b'

theorem BSeries.Series.convolution_left_eq_of_agreeUpToOrder_all {R : Type u} [CommSemiring R] {a a' b : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) : a.convolution b = a'.convolution b

theorem BSeries.Series.convolution_right_eq_of_agreeUpToOrder_all {R : Type u} [CommSemiring R] {a b b' : Series R} (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) : a.convolution b = a.convolution b'

theorem BSeries.Series.agreeUpToOrder_all_convolution {R : Type u} [CommSemiring R] {a a' b b' : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) (n : ℕ) : (a.convolution b).AgreeUpToOrder (a'.convolution b') n

theorem BSeries.Series.agreeUpToOrder_all_convolution_left {R : Type u} [CommSemiring R] {a a' b : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) (n : ℕ) : (a.convolution b).AgreeUpToOrder (a'.convolution b) n

theorem BSeries.Series.agreeUpToOrder_all_convolution_right {R : Type u} [CommSemiring R] {a b b' : Series R} (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) (n : ℕ) : (a.convolution b).AgreeUpToOrder (a.convolution b') n

theorem BSeries.Series.convolution_unit_right {R : Type u} [CommSemiring R] {a : Series R} (ha : a.HasUnitConstant) : a.convolution (unit R) = a

theorem BSeries.Series.convolution_unit_left {R : Type u} [CommSemiring R] {a : Series R} (ha : a.HasUnitConstant) : (unit R).convolution a = a

@[implicit_reducible]

noncomputable instance BSeries.Series.instUnitConstantMonoid {R : Type u} [CommSemiring R] : Monoid { a : Series R // a.HasUnitConstant }

Equations

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

noncomputable def BSeries.Series.characterMulEquiv {R : Type u} [CommSemiring R] : { a : Series R // a.HasUnitConstant } ≃* HopfAlgebras.ForestAlgebra.Character R

Equations

• BSeries.Series.characterMulEquiv = { toEquiv := BSeries.Series.characterEquiv, map_mul' := ⋯ }

@[simp]

theorem BSeries.Series.planarConvolutionForestCoeff_nil {R : Type u} [CommSemiring R] (a b : Series R) : a.planarConvolutionForestCoeff b [] = 1

@[simp]

theorem BSeries.Series.planarConvolutionForestCoeff_cons {R : Type u} [CommSemiring R] (a b : Series R) (t : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : a.planarConvolutionForestCoeff b (t :: ts) = a.planarConvolutionCoeff b t * a.planarConvolutionForestCoeff b ts

theorem BSeries.Series.planarConvolutionForestCoeff_perm {R : Type u} [CommSemiring R] (a b : Series R) {ts us : List HopfAlgebras.PTree} (h : ts.Perm us) : a.planarConvolutionForestCoeff b ts = a.planarConvolutionForestCoeff b us

theorem BSeries.Series.planarConvolutionForestCoeff_forall₂_perm {R : Type u} [CommSemiring R] (a b : Series R) {ts us : List HopfAlgebras.PTree} : List.Forall₂ HopfAlgebras.PTree.Perm ts us → a.planarConvolutionForestCoeff b ts = a.planarConvolutionForestCoeff b us

theorem BSeries.Series.convolution_hasOrder_zero {R : Type u} [Field R] (a b : Series R) : (a.convolution b).HasOrder 0

theorem BSeries.Series.convolution_hasOrder_all_congr {R : Type u} [Field R] {a a' b b' : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) : (∀ (n : ℕ), (a.convolution b).HasOrder n) ↔ ∀ (n : ℕ), (a'.convolution b').HasOrder n

theorem BSeries.Series.convolution_hasOrder_congr {R : Type u} [Field R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) : (a.convolution b).HasOrder n ↔ (a'.convolution b').HasOrder n

theorem BSeries.Series.convolution_hasOrder_all_congr_left {R : Type u} [Field R] {a a' b : Series R} (ha : ∀ (n : ℕ), a.AgreeUpToOrder a' n) : (∀ (n : ℕ), (a.convolution b).HasOrder n) ↔ ∀ (n : ℕ), (a'.convolution b).HasOrder n

theorem BSeries.Series.convolution_hasOrder_congr_left {R : Type u} [Field R] {a a' b : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) : (a.convolution b).HasOrder n ↔ (a'.convolution b).HasOrder n

theorem BSeries.Series.convolution_hasOrder_all_congr_right {R : Type u} [Field R] {a b b' : Series R} (hb : ∀ (n : ℕ), b.AgreeUpToOrder b' n) : (∀ (n : ℕ), (a.convolution b).HasOrder n) ↔ ∀ (n : ℕ), (a.convolution b').HasOrder n

theorem BSeries.Series.convolution_hasOrder_congr_right {R : Type u} [Field R] {a b b' : Series R} {n : ℕ} (hb : b.AgreeUpToOrder b' n) : (a.convolution b).HasOrder n ↔ (a.convolution b').HasOrder n

theorem BSeries.Series.convolution_unit_right_of_hasOrder {R : Type u} [Field R] {a : Series R} {n : ℕ} (ha : a.HasOrder n) : a.convolution (unit R) = a

theorem BSeries.Series.convolution_unit_left_of_hasOrder {R : Type u} [Field R] {a : Series R} {n : ℕ} (ha : a.HasOrder n) : (unit R).convolution a = a