B-Series

This file defines B-series and their algebraic structure.

Main definitions

• Series - coefficient families indexed by rooted trees
• Series.toCharacter - multiplicative extension to the rooted-forest algebra
• Series.characterEquiv - equivalence between unit-constant series and forest characters
• Series.unit - convolution identity coefficients
• Series.exact - exact-flow B-series coefficients
• Series.scaledExact - exact-flow coefficients with a time/step-size parameter
• Series.AgreeUpToOrder - coefficient agreement through a tree order
• Series.HasOrder - order conditions relative to the exact-flow coefficients

References

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

@[reducible, inline]

abbrev BSeries.Series (R : Type u) : Type u

A B-series over R, represented by its coefficients indexed by TreeIndex.

Equations

• BSeries.Series R = (HopfAlgebras.TreeIndex → R)

def BSeries.Series.coeff {R : Type u} (a : Series R) (τ : HopfAlgebras.TreeIndex) : R

The coefficient of a rooted tree index in a B-series.

Equations

• a.coeff τ = a τ

@[simp]

theorem BSeries.Series.coeff_apply {R : Type u} (a : Series R) (τ : HopfAlgebras.TreeIndex) : a.coeff τ = a τ

theorem BSeries.Series.ext {R : Type u} {a b : Series R} (h : ∀ (τ : HopfAlgebras.TreeIndex), a.coeff τ = b.coeff τ) : a = b

theorem BSeries.Series.ext_iff {R : Type u} {a b : Series R} : a = b ↔ ∀ (τ : HopfAlgebras.TreeIndex), a.coeff τ = b.coeff τ

def BSeries.Series.constantCoeff {R : Type u} (a : Series R) : R

The coefficient of the empty tree.

Equations

• a.constantCoeff = a.coeff HopfAlgebras.TreeIndex.empty

@[simp]

theorem BSeries.Series.coeff_empty {R : Type u} (a : Series R) : a.coeff HopfAlgebras.TreeIndex.empty = a.constantCoeff

@[simp]

theorem BSeries.Series.coeff_zero {R : Type u} [Zero R] (τ : HopfAlgebras.TreeIndex) : coeff 0 τ = 0

@[simp]

theorem BSeries.Series.coeff_add {R : Type u} [Add R] (a b : Series R) (τ : HopfAlgebras.TreeIndex) : (a + b).coeff τ = a.coeff τ + b.coeff τ

@[simp]

theorem BSeries.Series.coeff_neg {R : Type u} [Neg R] (a : Series R) (τ : HopfAlgebras.TreeIndex) : (-a).coeff τ = -a.coeff τ

@[simp]

theorem BSeries.Series.coeff_sub {R : Type u} [Sub R] (a b : Series R) (τ : HopfAlgebras.TreeIndex) : (a - b).coeff τ = a.coeff τ - b.coeff τ

@[simp]

theorem BSeries.Series.coeff_smul {R : Type u} {S : Type v} [SMul S R] (c : S) (a : Series R) (τ : HopfAlgebras.TreeIndex) : (c • a).coeff τ = c • a.coeff τ

@[simp]

theorem BSeries.Series.constantCoeff_zero {R : Type u} [Zero R] : constantCoeff 0 = 0

@[simp]

theorem BSeries.Series.constantCoeff_add {R : Type u} [Add R] (a b : Series R) : (a + b).constantCoeff = a.constantCoeff + b.constantCoeff

@[simp]

theorem BSeries.Series.constantCoeff_neg {R : Type u} [Neg R] (a : Series R) : (-a).constantCoeff = -a.constantCoeff

@[simp]

theorem BSeries.Series.constantCoeff_sub {R : Type u} [Sub R] (a b : Series R) : (a - b).constantCoeff = a.constantCoeff - b.constantCoeff

@[simp]

theorem BSeries.Series.constantCoeff_smul {R : Type u} {S : Type v} [SMul S R] (c : S) (a : Series R) : (c • a).constantCoeff = c • a.constantCoeff

def BSeries.Series.HasUnitConstant {R : Type u} [One R] (a : Series R) : Prop

The condition a(∅) = 1, used for B-series considered as maps.

Equations

• a.HasUnitConstant = (a.constantCoeff = 1)

theorem BSeries.Series.HasUnitConstant.coeff_empty {R : Type u} [One R] {a : Series R} (h : a.HasUnitConstant) : a.coeff HopfAlgebras.TreeIndex.empty = 1

def BSeries.Series.HasZeroConstant {R : Type u} [Zero R] (a : Series R) : Prop

The condition a(∅) = 0, used for B-series considered as vector fields.

Equations

• a.HasZeroConstant = (a.constantCoeff = 0)

theorem BSeries.Series.HasZeroConstant.coeff_empty {R : Type u} [Zero R] {a : Series R} (h : a.HasZeroConstant) : a.coeff HopfAlgebras.TreeIndex.empty = 0

theorem BSeries.Series.zero_hasZeroConstant {R : Type u} [Zero R] : HasZeroConstant 0

theorem BSeries.Series.HasZeroConstant.add {R : Type u} [AddMonoid R] {a b : Series R} (ha : a.HasZeroConstant) (hb : b.HasZeroConstant) : (a + b).HasZeroConstant

theorem BSeries.Series.HasZeroConstant.neg {R : Type u} [AddGroup R] {a : Series R} (ha : a.HasZeroConstant) : (-a).HasZeroConstant

theorem BSeries.Series.HasZeroConstant.sub {R : Type u} [AddGroup R] {a b : Series R} (ha : a.HasZeroConstant) (hb : b.HasZeroConstant) : (a - b).HasZeroConstant

theorem BSeries.Series.HasZeroConstant.smul {R : Type u} {S : Type v} [Zero R] [SMulZeroClass S R] {a : Series R} (c : S) (ha : a.HasZeroConstant) : (c • a).HasZeroConstant

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

Multiplicative coefficient of a rooted forest induced by a tree-indexed series.

Equations

• a.forestCoeff φ = (Multiset.map (fun (τ : HopfAlgebras.RootedTree) => a.coeff (HopfAlgebras.TreeIndex.tree τ)) φ).prod

@[simp]

theorem BSeries.Series.forestCoeff_zero {R : Type u} [CommSemiring R] (a : Series R) : a.forestCoeff 0 = 1

@[simp]

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

@[simp]

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

@[simp]

theorem BSeries.Series.forestCoeff_singleton_mset {R : Type u} [CommSemiring R] (a : Series R) (τ : HopfAlgebras.RootedTree) : a.forestCoeff {τ} = a.coeff (HopfAlgebras.TreeIndex.tree τ)

@[simp]

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

noncomputable def BSeries.Series.toCharacter {R : Type u} [CommSemiring R] (a : Series R) : HopfAlgebras.ForestAlgebra.Character R

The forest-algebra character induced by the tree coefficients of a series.

Equations

• a.toCharacter = (AddMonoidAlgebra.lift R R HopfAlgebras.RootedForest) (BSeries.Series.forestCoeffMonoidHom✝ a)

@[simp]

theorem BSeries.Series.toCharacter_ofForest {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = a.forestCoeff φ

@[simp]

theorem BSeries.Series.toCharacter_evalForest {R : Type u} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.RootedForest) : a.toCharacter.evalForest φ = a.forestCoeff φ

@[simp]

theorem BSeries.Series.toCharacter_ofForest_zero {R : Type u} [CommSemiring R] (a : Series R) : a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest 0) = 1

@[simp]

theorem BSeries.Series.toCharacter_ofForest_singleton {R : Type u} [CommSemiring R] (a : Series R) (τ : HopfAlgebras.RootedTree) : a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest (HopfAlgebras.RootedForest.singleton τ)) = a.coeff (HopfAlgebras.TreeIndex.tree τ)

theorem BSeries.Series.ext_of_toCharacter_eq {R : Type u} [CommSemiring R] {a b : Series R} (ha : a.HasUnitConstant) (hb : b.HasUnitConstant) (h : a.toCharacter = b.toCharacter) : a = b

Unit-constant series are determined by their induced forest-algebra characters.

theorem BSeries.Series.toCharacter_eq_iff {R : Type u} [CommSemiring R] {a b : Series R} (ha : a.HasUnitConstant) (hb : b.HasUnitConstant) : a.toCharacter = b.toCharacter ↔ a = b

noncomputable def BSeries.Series.ofCharacter {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : Series R

Recover the unit-constant B-series determined by a forest-algebra character.

Equations

• BSeries.Series.ofCharacter χ HopfAlgebras.TreeIndex.empty = 1
• BSeries.Series.ofCharacter χ (HopfAlgebras.TreeIndex.tree τ) = χ.evalForest (HopfAlgebras.RootedForest.singleton τ)

@[simp]

theorem BSeries.Series.ofCharacter_empty {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : (ofCharacter χ).coeff HopfAlgebras.TreeIndex.empty = 1

@[simp]

theorem BSeries.Series.ofCharacter_tree {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) (τ : HopfAlgebras.RootedTree) : (ofCharacter χ).coeff (HopfAlgebras.TreeIndex.tree τ) = χ.evalForest (HopfAlgebras.RootedForest.singleton τ)

theorem BSeries.Series.ofCharacter_hasUnitConstant {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : (ofCharacter χ).HasUnitConstant

@[simp]

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

theorem BSeries.Series.ofCharacter_toCharacter {R : Type u} [CommSemiring R] {a : Series R} (ha : a.HasUnitConstant) : ofCharacter a.toCharacter = a

theorem BSeries.Series.forestCoeff_ofCharacter {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) (φ : HopfAlgebras.RootedForest) : (ofCharacter χ).forestCoeff φ = χ.evalForest φ

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

Unit-constant B-series are equivalent to forest-algebra characters.

Equations

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

@[simp]

theorem BSeries.Series.characterEquiv_apply {R : Type u} [CommSemiring R] (a : { a : Series R // a.HasUnitConstant }) : characterEquiv a = (↑a).toCharacter

@[simp]

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

theorem BSeries.Series.characterEquiv_symm_forestCoeff {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) (φ : HopfAlgebras.RootedForest) : (↑(characterEquiv.symm χ)).forestCoeff φ = χ.evalForest φ

def BSeries.Series.unit (R : Type u) [Zero R] [One R] : Series R

The convolution identity B-series: 1 on the empty tree and 0 on every tree.

Equations

• BSeries.Series.unit R HopfAlgebras.TreeIndex.empty = 1
• BSeries.Series.unit R (HopfAlgebras.TreeIndex.tree τ) = 0

@[simp]

theorem BSeries.Series.coeff_unit_empty {R : Type u} [Zero R] [One R] : (unit R).coeff HopfAlgebras.TreeIndex.empty = 1

@[simp]

theorem BSeries.Series.coeff_unit_tree {R : Type u} [Zero R] [One R] (τ : HopfAlgebras.RootedTree) : (unit R).coeff (HopfAlgebras.TreeIndex.tree τ) = 0

theorem BSeries.Series.unit_hasUnitConstant {R : Type u} [Zero R] [One R] : (unit R).HasUnitConstant

theorem BSeries.Series.forestCoeff_unit {R : Type u} [CommSemiring R] (φ : HopfAlgebras.RootedForest) : (unit R).forestCoeff φ = HopfAlgebras.ForestAlgebra.counitCoeff φ

@[simp]

theorem BSeries.Series.toCharacter_unit_ofForest {R : Type u} [CommSemiring R] (φ : HopfAlgebras.RootedForest) : (unit R).toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = HopfAlgebras.ForestAlgebra.counitCoeff φ

theorem BSeries.Series.toCharacter_unit {R : Type u} [CommSemiring R] : (unit R).toCharacter = HopfAlgebras.ForestAlgebra.counit R

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

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

theorem BSeries.Series.characterEquiv_symm_counit {R : Type u} [CommSemiring R] : ↑(characterEquiv.symm (HopfAlgebras.ForestAlgebra.counit R)) = unit R

def BSeries.Series.exact (R : Type u) [DivisionSemiring R] : Series R

Exact-flow B-series coefficients, recursively given by the inverse tree factorial.

Equations

• BSeries.Series.exact R τ = (↑τ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.coeff_exact {R : Type u} [DivisionSemiring R] (τ : HopfAlgebras.TreeIndex) : (exact R).coeff τ = (↑τ.treeFactorial)⁻¹

def BSeries.Series.scaledExact {R : Type u} [DivisionSemiring R] (h : R) : Series R

Exact-flow B-series coefficients at time/step-size h.

Equations

• BSeries.Series.scaledExact h τ = h ^ τ.order * (↑τ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.coeff_scaledExact {R : Type u} [DivisionSemiring R] (h : R) (τ : HopfAlgebras.TreeIndex) : (scaledExact h).coeff τ = h ^ τ.order * (↑τ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.scaledExact_one {R : Type u} [DivisionSemiring R] : scaledExact 1 = exact R

@[simp]

theorem BSeries.Series.scaledExact_zero {R : Type u} [DivisionSemiring R] : scaledExact 0 = unit R

theorem BSeries.Series.scaledExact_hasUnitConstant {R : Type u} [DivisionSemiring R] (h : R) : (scaledExact h).HasUnitConstant

theorem BSeries.Series.coeff_exact_tree_graft {R : Type u} [Field R] (φ : HopfAlgebras.RootedForest) : (exact R).coeff (HopfAlgebras.TreeIndex.tree φ.graft) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.coeff_scaledExact_tree_graft {R : Type u} [Field R] (h : R) (φ : HopfAlgebras.RootedForest) : (scaledExact h).coeff (HopfAlgebras.TreeIndex.tree φ.graft) = h ^ (1 + φ.order) * (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.coeff_exact_tree_branches {R : Type u} [Field R] (τ : HopfAlgebras.RootedTree) : (exact R).coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.Series.coeff_scaledExact_tree_branches {R : Type u} [Field R] (h : R) (τ : HopfAlgebras.RootedTree) : (scaledExact h).coeff (HopfAlgebras.TreeIndex.tree τ) = h ^ τ.order * (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.Series.coeff_exact_tree_butcherProduct {R : Type u} [Field R] (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree) : (exact R).coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.Series.coeff_scaledExact_tree_butcherProduct {R : Type u} [Field R] (h : R) (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree) : (scaledExact h).coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = h ^ (φ.order + τ.order) * (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.Series.exact_hasUnitConstant {R : Type u} [DivisionSemiring R] : (exact R).HasUnitConstant

theorem BSeries.Series.forestCoeff_exact {R : Type u} [Field R] (φ : HopfAlgebras.RootedForest) : (exact R).forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.forestCoeff_scaledExact {R : Type u} [Field R] (h : R) (φ : HopfAlgebras.RootedForest) : (scaledExact h).forestCoeff φ = h ^ φ.order * (↑φ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.forestCoeff_scaledExact_zero {R : Type u} [Field R] (φ : HopfAlgebras.RootedForest) : (scaledExact 0).forestCoeff φ = HopfAlgebras.ForestAlgebra.counitCoeff φ

@[simp]

theorem BSeries.Series.toCharacter_exact_ofForest {R : Type u} [Field R] (φ : HopfAlgebras.RootedForest) : (exact R).toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.toCharacter_scaledExact_ofForest {R : Type u} [Field R] (h : R) (φ : HopfAlgebras.RootedForest) : (scaledExact h).toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = h ^ φ.order * (↑φ.treeFactorial)⁻¹

@[simp]

theorem BSeries.Series.toCharacter_scaledExact_zero {R : Type u} [Field R] : (scaledExact 0).toCharacter = HopfAlgebras.ForestAlgebra.counit R

def BSeries.Series.AgreeUpToOrder {R : Type u} (a b : Series R) (n : ℕ) : Prop

Two B-series agree through order n if their coefficients agree on all trees of order at most n.

Equations

• a.AgreeUpToOrder b n = ∀ (τ : HopfAlgebras.TreeIndex), τ.order ≤ n → a.coeff τ = b.coeff τ

theorem BSeries.Series.agreeUpToOrder_refl {R : Type u} (a : Series R) (n : ℕ) : a.AgreeUpToOrder a n

theorem BSeries.Series.AgreeUpToOrder.symm {R : Type u} {a b : Series R} {n : ℕ} (h : a.AgreeUpToOrder b n) : b.AgreeUpToOrder a n

theorem BSeries.Series.AgreeUpToOrder.trans {R : Type u} {a b c : Series R} {n : ℕ} (hab : a.AgreeUpToOrder b n) (hbc : b.AgreeUpToOrder c n) : a.AgreeUpToOrder c n

theorem BSeries.Series.AgreeUpToOrder.mono {R : Type u} {a b : Series R} {m n : ℕ} (h : a.AgreeUpToOrder b n) (hmn : m ≤ n) : a.AgreeUpToOrder b m

theorem BSeries.Series.agreeUpToOrder_succ_iff {R : Type u} {a b : Series R} {n : ℕ} : a.AgreeUpToOrder b (n + 1) ↔ a.AgreeUpToOrder b n ∧ ∀ (τ : HopfAlgebras.TreeIndex), τ.order = n + 1 → a.coeff τ = b.coeff τ

theorem BSeries.Series.AgreeUpToOrder.add {R : Type u} [Add R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) : (a + b).AgreeUpToOrder (a' + b') n

theorem BSeries.Series.AgreeUpToOrder.neg {R : Type u} [Neg R] {a b : Series R} {n : ℕ} (h : a.AgreeUpToOrder b n) : (-a).AgreeUpToOrder (-b) n

theorem BSeries.Series.AgreeUpToOrder.sub {R : Type u} [Sub R] {a a' b b' : Series R} {n : ℕ} (ha : a.AgreeUpToOrder a' n) (hb : b.AgreeUpToOrder b' n) : (a - b).AgreeUpToOrder (a' - b') n

theorem BSeries.Series.AgreeUpToOrder.smul {R : Type u} {S : Type v} [SMul S R] {a b : Series R} {n : ℕ} (c : S) (h : a.AgreeUpToOrder b n) : (c • a).AgreeUpToOrder (c • b) n

theorem BSeries.Series.agreeUpToOrder_iff_treeCoeff {R : Type u} {a b : Series R} {n : ℕ} : a.AgreeUpToOrder b n ↔ a.constantCoeff = b.constantCoeff ∧ ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → a.coeff (HopfAlgebras.TreeIndex.tree τ) = b.coeff (HopfAlgebras.TreeIndex.tree τ)

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

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

theorem BSeries.Series.AgreeUpToOrder.toCharacter_ofForest {R : Type u} [CommSemiring R] {a b : Series R} {n : ℕ} (h : a.AgreeUpToOrder b n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = b.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ)

theorem BSeries.Series.agreeUpToOrder_iff_forestCoeff {R : Type u} [CommSemiring R] {a b : Series R} {n : ℕ} : a.AgreeUpToOrder b n ↔ a.constantCoeff = b.constantCoeff ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.forestCoeff φ = b.forestCoeff φ

theorem BSeries.Series.agreeUpToOrder_iff_toCharacter_evalForest {R : Type u} [CommSemiring R] {a b : Series R} {n : ℕ} : a.AgreeUpToOrder b n ↔ a.constantCoeff = b.constantCoeff ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.toCharacter.evalForest φ = b.toCharacter.evalForest φ

theorem BSeries.Series.agreeUpToOrder_iff_toCharacter_ofForest {R : Type u} [CommSemiring R] {a b : Series R} {n : ℕ} : a.AgreeUpToOrder b n ↔ a.constantCoeff = b.constantCoeff ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = b.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ)

theorem BSeries.Series.agreeUpToOrder_of_eq {R : Type u} {a b : Series R} (h : a = b) (n : ℕ) : a.AgreeUpToOrder b n

theorem BSeries.Series.eq_of_agreeUpToOrder_all {R : Type u} {a b : Series R} (h : ∀ (n : ℕ), a.AgreeUpToOrder b n) : a = b

theorem BSeries.Series.agreeUpToOrder_all_iff_eq {R : Type u} {a b : Series R} : (∀ (n : ℕ), a.AgreeUpToOrder b n) ↔ a = b

theorem BSeries.Series.agreeUpToOrder_all_iff_constantCoeff_toCharacter {R : Type u} [CommSemiring R] {a b : Series R} : (∀ (n : ℕ), a.AgreeUpToOrder b n) ↔ a.constantCoeff = b.constantCoeff ∧ a.toCharacter = b.toCharacter

def BSeries.Series.HasOrder {R : Type u} [DivisionSemiring R] (a : Series R) (n : ℕ) : Prop

Coefficient-level order conditions for a B-series.

Equations

• a.HasOrder n = a.AgreeUpToOrder (BSeries.Series.exact R) n

theorem BSeries.Series.hasOrder_iff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ ∀ (τ : HopfAlgebras.TreeIndex), τ.order ≤ n → a.coeff τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.coeff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {τ : HopfAlgebras.TreeIndex} (hτ : τ.order ≤ n) : a.coeff τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.treeCoeff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.coeff_tree_graft {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : 1 + φ.order ≤ n) : a.coeff (HopfAlgebras.TreeIndex.tree φ.graft) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.coeff_tree_branches {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.hasUnitConstant {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} (h : a.HasOrder n) : a.HasUnitConstant

theorem BSeries.Series.hasOrder_iff_treeCoeff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.mono {R : Type u} [DivisionSemiring R] {a : Series R} {m n : ℕ} (h : a.HasOrder n) (hmn : m ≤ n) : a.HasOrder m

theorem BSeries.Series.hasOrder_succ_iff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} : a.HasOrder (n + 1) ↔ a.HasOrder n ∧ ∀ (τ : HopfAlgebras.TreeIndex), τ.order = n + 1 → a.coeff τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.of_agreeUpToOrder {R : Type u} [DivisionSemiring R] {a b : Series R} {n : ℕ} (hab : a.AgreeUpToOrder b n) (ha : a.HasOrder n) : b.HasOrder n

theorem BSeries.Series.hasOrder_congr {R : Type u} [DivisionSemiring R] {a b : Series R} {n : ℕ} (hab : a.AgreeUpToOrder b n) : a.HasOrder n ↔ b.HasOrder n

theorem BSeries.Series.hasOrder_all_congr {R : Type u} [DivisionSemiring R] {a b : Series R} (hab : ∀ (n : ℕ), a.AgreeUpToOrder b n) : (∀ (n : ℕ), a.HasOrder n) ↔ ∀ (n : ℕ), b.HasOrder n

theorem BSeries.Series.HasOrder.agreeUpToOrder {R : Type u} [DivisionSemiring R] {a b : Series R} {n : ℕ} (ha : a.HasOrder n) (hb : b.HasOrder n) : a.AgreeUpToOrder b n

theorem BSeries.Series.hasOrder_zero_iff {R : Type u} [DivisionSemiring R] {a : Series R} : a.HasOrder 0 ↔ a.HasUnitConstant

theorem BSeries.Series.HasOrder.bulletCoeff {R : Type u} [DivisionSemiring R] {a : Series R} {n : ℕ} (h : a.HasOrder n) (hn : 1 ≤ n) : a.coeff HopfAlgebras.TreeIndex.bullet = 1

theorem BSeries.Series.hasOrder_one_iff {R : Type u} [DivisionSemiring R] {a : Series R} : a.HasOrder 1 ↔ a.HasUnitConstant ∧ a.coeff HopfAlgebras.TreeIndex.bullet = 1

theorem BSeries.Series.exact_hasOrder {R : Type u} [DivisionSemiring R] (n : ℕ) : (exact R).HasOrder n

theorem BSeries.Series.eq_exact_of_hasOrder_all {R : Type u} [DivisionSemiring R] {a : Series R} (h : ∀ (n : ℕ), a.HasOrder n) : a = exact R

theorem BSeries.Series.hasOrder_all_iff_eq_exact {R : Type u} [DivisionSemiring R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a = exact R

theorem BSeries.Series.hasOrder_all_iff_treeCoeff {R : Type u} [DivisionSemiring R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (τ : HopfAlgebras.RootedTree), a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_forestCoeff {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_toCharacter_evalForest {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_toCharacter_ofForest {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.forestCoeff {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : a.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.toCharacter_evalForest {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : a.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.toCharacter_ofForest {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_coeff_tree_graft {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), 1 + φ.order ≤ n → a.coeff (HopfAlgebras.TreeIndex.tree φ.graft) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_coeff_tree_branches {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.Series.HasOrder.coeff_butcherProduct {R : Type u} [Field R] {a : Series R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.RootedForest} {τ : HopfAlgebras.RootedTree} (horder : φ.order + τ.order ≤ n) : a.coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_iff_coeff_butcherProduct {R : Type u} [Field R] {a : Series R} {n : ℕ} : a.HasOrder n ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree), φ.order + τ.order ≤ n → a.coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_forestCoeff {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), a.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_coeff_tree_graft {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), a.coeff (HopfAlgebras.TreeIndex.tree φ.graft) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_coeff_tree_branches {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (τ : HopfAlgebras.RootedTree), a.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_toCharacter_evalForest {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), a.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_toCharacter_ofForest {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest), a.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.Series.hasOrder_all_iff_toCharacter_eq_exact {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ a.toCharacter = (exact R).toCharacter

theorem BSeries.Series.characterEquiv_hasOrder_all_iff_exact {R : Type u} [Field R] (a : { a : Series R // a.HasUnitConstant }) : (∀ (n : ℕ), (↑a).HasOrder n) ↔ characterEquiv a = characterEquiv ⟨exact R, ⋯⟩

theorem BSeries.Series.hasOrder_all_iff_coeff_butcherProduct {R : Type u} [Field R] {a : Series R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree), a.coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹