Labelled B-Series

This file defines labelled B-series coefficient families and their multiplicative extension to the labelled rooted-forest algebra.

Main definitions

• LTreeIndex α - labelled rooted trees with an adjoined empty tree
• LSeries α R - coefficient families indexed by labelled rooted trees
• LSeries.toCharacter - multiplicative extension to labelled forest characters
• LSeries.ofCharacter - recover labelled coefficients from a forest character
• LSeries.characterEquiv - equivalence between unit-constant series and characters
• LSeries.unit - convolution identity coefficients
• LSeries.exact - exact-flow coefficients, ignoring labels
• LSeries.scaledExact - exact-flow coefficients with a time/step-size parameter
• LSeries.AgreeUpToOrder - coefficient agreement through a labelled tree order
• LSeries.HasOrder - order conditions relative to exact labelled coefficients
• LSeries.comapMapLabels - pull back labelled coefficients by relabelling
• LSeries.comapConstLabel - restrict labelled coefficients to one constant label
• LSeries.comapEraseLabels - pull back unlabelled coefficients by erasing labels
• LSeries.LabelInvariant - labelled coefficients that descend to unlabelled trees

inductive BSeries.LTreeIndex (α : Type u) : Type u

Labelled rooted trees with an adjoined empty tree.

• empty {α : Type u} : LTreeIndex α
• tree {α : Type u} : HopfAlgebras.LRootedTree α → LTreeIndex α

def BSeries.LTreeIndex.order {α : Type u} : LTreeIndex α → ℕ

The order of a labelled B-series tree index.

Equations

• BSeries.LTreeIndex.empty.order = 0
• (BSeries.LTreeIndex.tree τ).order = τ.order

def BSeries.LTreeIndex.IsOfOrder {α : Type u} (τ : LTreeIndex α) (n : ℕ) : Prop

Predicate for labelled B-series tree indices of a fixed order.

Equations

• τ.IsOfOrder n = (τ.order = n)

def BSeries.LTreeIndex.treeFactorial {α : Type u} : LTreeIndex α → ℕ

Butcher's tree factorial for labelled B-series tree indices.

Equations

• BSeries.LTreeIndex.empty.treeFactorial = 1
• (BSeries.LTreeIndex.tree τ).treeFactorial = τ.treeFactorial

def BSeries.LTreeIndex.erase {α : Type u} : LTreeIndex α → HopfAlgebras.TreeIndex

Forget labels from a labelled B-series tree index.

Equations

• BSeries.LTreeIndex.empty.erase = HopfAlgebras.TreeIndex.empty
• (BSeries.LTreeIndex.tree τ).erase = HopfAlgebras.TreeIndex.tree τ.erase

def BSeries.LTreeIndex.mapLabels {α : Type u} {β : Type v} (f : α → β) : LTreeIndex α → LTreeIndex β

Relabel a labelled B-series tree index.

Equations

• BSeries.LTreeIndex.mapLabels f BSeries.LTreeIndex.empty = BSeries.LTreeIndex.empty
• BSeries.LTreeIndex.mapLabels f (BSeries.LTreeIndex.tree τ) = BSeries.LTreeIndex.tree (HopfAlgebras.LRootedTree.map f τ)

def BSeries.LTreeIndex.constLabel {α : Type u} (a : α) : HopfAlgebras.TreeIndex → LTreeIndex α

Label every vertex of an unlabelled B-series tree index by the same label.

Equations

• BSeries.LTreeIndex.constLabel a HopfAlgebras.TreeIndex.empty = BSeries.LTreeIndex.empty
• BSeries.LTreeIndex.constLabel a (HopfAlgebras.TreeIndex.tree τ) = BSeries.LTreeIndex.tree (HopfAlgebras.LRootedTree.constLabel a τ)

@[simp]

theorem BSeries.LTreeIndex.order_empty {α : Type u} : empty.order = 0

@[simp]

theorem BSeries.LTreeIndex.order_tree {α : Type u} (τ : HopfAlgebras.LRootedTree α) : (tree τ).order = τ.order

@[simp]

theorem BSeries.LTreeIndex.treeFactorial_empty {α : Type u} : empty.treeFactorial = 1

@[simp]

theorem BSeries.LTreeIndex.treeFactorial_tree {α : Type u} (τ : HopfAlgebras.LRootedTree α) : (tree τ).treeFactorial = τ.treeFactorial

@[simp]

theorem BSeries.LTreeIndex.erase_empty {α : Type u} : empty.erase = HopfAlgebras.TreeIndex.empty

@[simp]

theorem BSeries.LTreeIndex.erase_tree {α : Type u} (τ : HopfAlgebras.LRootedTree α) : (tree τ).erase = HopfAlgebras.TreeIndex.tree τ.erase

@[simp]

theorem BSeries.LTreeIndex.constLabel_empty {α : Type u} (a : α) : constLabel a HopfAlgebras.TreeIndex.empty = empty

@[simp]

theorem BSeries.LTreeIndex.constLabel_tree {α : Type u} (a : α) (τ : HopfAlgebras.RootedTree) : constLabel a (HopfAlgebras.TreeIndex.tree τ) = tree (HopfAlgebras.LRootedTree.constLabel a τ)

@[simp]

theorem BSeries.LTreeIndex.mapLabels_empty {α : Type u} {β : Type v} (f : α → β) : mapLabels f empty = empty

@[simp]

theorem BSeries.LTreeIndex.mapLabels_tree {α : Type u} {β : Type v} (f : α → β) (τ : HopfAlgebras.LRootedTree α) : mapLabels f (tree τ) = tree (HopfAlgebras.LRootedTree.map f τ)

@[simp]

theorem BSeries.LTreeIndex.order_erase {α : Type u} (τ : LTreeIndex α) : τ.erase.order = τ.order

@[simp]

theorem BSeries.LTreeIndex.treeFactorial_erase {α : Type u} (τ : LTreeIndex α) : τ.erase.treeFactorial = τ.treeFactorial

@[simp]

theorem BSeries.LTreeIndex.erase_constLabel {α : Type u} (a : α) (τ : HopfAlgebras.TreeIndex) : (constLabel a τ).erase = τ

theorem BSeries.LTreeIndex.constLabel_injective {α : Type u} (a : α) : Function.Injective (constLabel a)

@[simp]

theorem BSeries.LTreeIndex.constLabel_eq_constLabel_iff {α : Type u} (a : α) {σ τ : HopfAlgebras.TreeIndex} : constLabel a σ = constLabel a τ ↔ σ = τ

@[simp]

theorem BSeries.LTreeIndex.order_mapLabels {α : Type u} {β : Type v} (f : α → β) (τ : LTreeIndex α) : (mapLabels f τ).order = τ.order

@[simp]

theorem BSeries.LTreeIndex.treeFactorial_mapLabels {α : Type u} {β : Type v} (f : α → β) (τ : LTreeIndex α) : (mapLabels f τ).treeFactorial = τ.treeFactorial

@[simp]

theorem BSeries.LTreeIndex.order_constLabel {α : Type u} (a : α) (τ : HopfAlgebras.TreeIndex) : (constLabel a τ).order = τ.order

@[simp]

theorem BSeries.LTreeIndex.treeFactorial_constLabel {α : Type u} (a : α) (τ : HopfAlgebras.TreeIndex) : (constLabel a τ).treeFactorial = τ.treeFactorial

@[simp]

theorem BSeries.LTreeIndex.erase_mapLabels {α : Type u} {β : Type v} (f : α → β) (τ : LTreeIndex α) : (mapLabels f τ).erase = τ.erase

@[simp]

theorem BSeries.LTreeIndex.mapLabels_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (τ : HopfAlgebras.TreeIndex) : mapLabels f (constLabel a τ) = constLabel (f a) τ

@[simp]

theorem BSeries.LTreeIndex.mapLabels_id {α : Type u} (τ : LTreeIndex α) : mapLabels id τ = τ

@[simp]

theorem BSeries.LTreeIndex.mapLabels_comp {α : Type u} {β : Type v} {γ : Type x} (g : β → γ) (f : α → β) (τ : LTreeIndex α) : mapLabels g (mapLabels f τ) = mapLabels (g ∘ f) τ

theorem BSeries.LTreeIndex.mapLabels_comp_eq_id {α : Type u} {β : Type v} (f : α → β) (g : β → α) (h : ∀ (x : β), f (g x) = x) (τ : LTreeIndex β) : mapLabels f (mapLabels g τ) = τ

theorem BSeries.LTreeIndex.mapLabels_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) : Function.Injective (mapLabels f)

theorem BSeries.LTreeIndex.mapLabels_eq_mapLabels_iff_of_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) {σ τ : LTreeIndex α} : mapLabels f σ = mapLabels f τ ↔ σ = τ

@[simp]

theorem BSeries.LTreeIndex.order_eq_zero_iff {α : Type u} (τ : LTreeIndex α) : τ.order = 0 ↔ τ = empty

theorem BSeries.LTreeIndex.order_pos_iff_ne_empty {α : Type u} (τ : LTreeIndex α) : 0 < τ.order ↔ τ ≠ empty

theorem BSeries.LTreeIndex.order_eq_one_iff_exists_tree_graft_zero {α : Type u} (τ : LTreeIndex α) : τ.order = 1 ↔ ∃ (a : α), τ = tree (HopfAlgebras.LRootedForest.graft a 0)

theorem BSeries.LTreeIndex.treeFactorial_pos {α : Type u} (τ : LTreeIndex α) : 0 < τ.treeFactorial

theorem BSeries.LTreeIndex.treeFactorial_ne_zero {α : Type u} (τ : LTreeIndex α) : τ.treeFactorial ≠ 0

@[reducible, inline]

abbrev BSeries.LSeries (α : Type u) (R : Type v) : Type (max u v)

A labelled B-series over R, represented by labelled-tree coefficients.

Equations

• BSeries.LSeries α R = (BSeries.LTreeIndex α → R)

def BSeries.LSeries.coeff {α : Type u} {R : Type w} (a : LSeries α R) (τ : LTreeIndex α) : R

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

Equations

• a.coeff τ = a τ

@[simp]

theorem BSeries.LSeries.coeff_apply {α : Type u} {R : Type w} (a : LSeries α R) (τ : LTreeIndex α) : a.coeff τ = a τ

theorem BSeries.LSeries.ext {α : Type u} {R : Type w} {a b : LSeries α R} (h : ∀ (τ : LTreeIndex α), a.coeff τ = b.coeff τ) : a = b

theorem BSeries.LSeries.ext_iff {α : Type u} {R : Type w} {a b : LSeries α R} : a = b ↔ ∀ (τ : LTreeIndex α), a.coeff τ = b.coeff τ

def BSeries.LSeries.constantCoeff {α : Type u} {R : Type w} (a : LSeries α R) : R

The coefficient of the empty labelled tree.

Equations

• a.constantCoeff = a.coeff BSeries.LTreeIndex.empty

@[simp]

theorem BSeries.LSeries.coeff_empty {α : Type u} {R : Type w} (a : LSeries α R) : a.coeff LTreeIndex.empty = a.constantCoeff

@[simp]

theorem BSeries.LSeries.coeff_zero {α : Type u} {R : Type w} [Zero R] (τ : LTreeIndex α) : coeff 0 τ = 0

@[simp]

theorem BSeries.LSeries.coeff_add {α : Type u} {R : Type w} [Add R] (a b : LSeries α R) (τ : LTreeIndex α) : (a + b).coeff τ = a.coeff τ + b.coeff τ

@[simp]

theorem BSeries.LSeries.coeff_neg {α : Type u} {R : Type w} [Neg R] (a : LSeries α R) (τ : LTreeIndex α) : (-a).coeff τ = -a.coeff τ

@[simp]

theorem BSeries.LSeries.coeff_sub {α : Type u} {R : Type w} [Sub R] (a b : LSeries α R) (τ : LTreeIndex α) : (a - b).coeff τ = a.coeff τ - b.coeff τ

@[simp]

theorem BSeries.LSeries.coeff_smul {α : Type u} {R : Type w} {S : Type y} [SMul S R] (c : S) (a : LSeries α R) (τ : LTreeIndex α) : (c • a).coeff τ = c • a.coeff τ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BSeries.LSeries.constantCoeff_smul {α : Type u} {R : Type w} {S : Type y} [SMul S R] (c : S) (a : LSeries α R) : (c • a).constantCoeff = c • a.constantCoeff

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

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

Equations

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

theorem BSeries.LSeries.HasUnitConstant.coeff_empty {α : Type u} {R : Type w} [One R] {a : LSeries α R} (h : a.HasUnitConstant) : a.coeff LTreeIndex.empty = 1

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

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

Equations

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

theorem BSeries.LSeries.HasZeroConstant.coeff_empty {α : Type u} {R : Type w} [Zero R] {a : LSeries α R} (h : a.HasZeroConstant) : a.coeff LTreeIndex.empty = 0

theorem BSeries.LSeries.zero_hasZeroConstant {α : Type u} {R : Type w} [Zero R] : HasZeroConstant 0

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

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

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

theorem BSeries.LSeries.HasZeroConstant.smul {α : Type u} {R : Type w} {S : Type y} [Zero R] [SMulZeroClass S R] {a : LSeries α R} (c : S) (ha : a.HasZeroConstant) : (c • a).HasZeroConstant

def BSeries.LSeries.forestCoeff {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (φ : HopfAlgebras.LRootedForest α) : R

Multiplicative coefficient of a labelled rooted forest induced by a series.

Equations

• a.forestCoeff φ = (Multiset.map (fun (τ : HopfAlgebras.LRootedTree α) => a.coeff (BSeries.LTreeIndex.tree τ)) φ).prod

@[simp]

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

@[simp]

theorem BSeries.LSeries.forestCoeff_empty {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) : a.forestCoeff HopfAlgebras.LRootedForest.empty = 1

@[simp]

theorem BSeries.LSeries.forestCoeff_singleton {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (τ : HopfAlgebras.LRootedTree α) : a.forestCoeff (HopfAlgebras.LRootedForest.singleton τ) = a.coeff (LTreeIndex.tree τ)

@[simp]

theorem BSeries.LSeries.forestCoeff_singleton_mset {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (τ : HopfAlgebras.LRootedTree α) : a.forestCoeff {τ} = a.coeff (LTreeIndex.tree τ)

@[simp]

theorem BSeries.LSeries.forestCoeff_add {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (φ ψ : HopfAlgebras.LRootedForest α) : a.forestCoeff (φ + ψ) = a.forestCoeff φ * a.forestCoeff ψ

noncomputable def BSeries.LSeries.toCharacter {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) : HopfAlgebras.LForestAlgebra.Character α R

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

Equations

• a.toCharacter = (AddMonoidAlgebra.lift R R (HopfAlgebras.LRootedForest α)) (BSeries.LSeries.forestCoeffMonoidHom✝ a)

@[simp]

theorem BSeries.LSeries.toCharacter_ofForest {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (φ : HopfAlgebras.LRootedForest α) : a.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = a.forestCoeff φ

@[simp]

theorem BSeries.LSeries.toCharacter_evalForest {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (φ : HopfAlgebras.LRootedForest α) : a.toCharacter.evalForest φ = a.forestCoeff φ

@[simp]

theorem BSeries.LSeries.toCharacter_ofForest_zero {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) : a.toCharacter (HopfAlgebras.LForestAlgebra.ofForest 0) = 1

@[simp]

theorem BSeries.LSeries.toCharacter_ofForest_singleton {α : Type u} {R : Type w} [CommSemiring R] (a : LSeries α R) (τ : HopfAlgebras.LRootedTree α) : a.toCharacter (HopfAlgebras.LForestAlgebra.ofForest (HopfAlgebras.LRootedForest.singleton τ)) = a.coeff (LTreeIndex.tree τ)

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

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

noncomputable def BSeries.LSeries.ofCharacter {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : LSeries α R

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

Equations

• BSeries.LSeries.ofCharacter χ BSeries.LTreeIndex.empty = 1
• BSeries.LSeries.ofCharacter χ (BSeries.LTreeIndex.tree τ) = χ.evalForest (HopfAlgebras.LRootedForest.singleton τ)

@[simp]

theorem BSeries.LSeries.ofCharacter_empty {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : (ofCharacter χ).coeff LTreeIndex.empty = 1

@[simp]

theorem BSeries.LSeries.ofCharacter_tree {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) (τ : HopfAlgebras.LRootedTree α) : (ofCharacter χ).coeff (LTreeIndex.tree τ) = χ.evalForest (HopfAlgebras.LRootedForest.singleton τ)

theorem BSeries.LSeries.ofCharacter_hasUnitConstant {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : (ofCharacter χ).HasUnitConstant

@[simp]

theorem BSeries.LSeries.toCharacter_ofCharacter {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : (ofCharacter χ).toCharacter = χ

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

theorem BSeries.LSeries.forestCoeff_ofCharacter {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) (φ : HopfAlgebras.LRootedForest α) : (ofCharacter χ).forestCoeff φ = χ.evalForest φ

noncomputable def BSeries.LSeries.characterEquiv {α : Type u} {R : Type w} [CommSemiring R] : { a : LSeries α R // a.HasUnitConstant } ≃ HopfAlgebras.LForestAlgebra.Character α R

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

Equations

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

@[simp]

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

@[simp]

theorem BSeries.LSeries.characterEquiv_symm_apply {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : ↑(characterEquiv.symm χ) = ofCharacter χ

theorem BSeries.LSeries.characterEquiv_symm_forestCoeff {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) (φ : HopfAlgebras.LRootedForest α) : (↑(characterEquiv.symm χ)).forestCoeff φ = χ.evalForest φ

def BSeries.LSeries.unit (α : Type u) (R : Type v) [Zero R] [One R] : LSeries α R

The labelled convolution identity coefficients.

Equations

• BSeries.LSeries.unit α R BSeries.LTreeIndex.empty = 1
• BSeries.LSeries.unit α R (BSeries.LTreeIndex.tree τ) = 0

@[simp]

theorem BSeries.LSeries.coeff_unit_empty {α : Type u} {R : Type w} [Zero R] [One R] : (unit α R).coeff LTreeIndex.empty = 1

@[simp]

theorem BSeries.LSeries.coeff_unit_tree {α : Type u} {R : Type w} [Zero R] [One R] (τ : HopfAlgebras.LRootedTree α) : (unit α R).coeff (LTreeIndex.tree τ) = 0

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

theorem BSeries.LSeries.forestCoeff_unit {α : Type u} {R : Type w} [CommSemiring R] (φ : HopfAlgebras.LRootedForest α) : (unit α R).forestCoeff φ = HopfAlgebras.LForestAlgebra.counitCoeff φ

@[simp]

theorem BSeries.LSeries.toCharacter_unit_ofForest {α : Type u} {R : Type w} [CommSemiring R] (φ : HopfAlgebras.LRootedForest α) : (unit α R).toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = HopfAlgebras.LForestAlgebra.counitCoeff φ

theorem BSeries.LSeries.toCharacter_unit {α : Type u} {R : Type w} [CommSemiring R] : (unit α R).toCharacter = HopfAlgebras.LForestAlgebra.counit α R

theorem BSeries.LSeries.ofCharacter_counit {α : Type u} {R : Type w} [CommSemiring R] : ofCharacter (HopfAlgebras.LForestAlgebra.counit α R) = unit α R

theorem BSeries.LSeries.characterEquiv_unit_counit {α : Type u} {R : Type w} [CommSemiring R] : characterEquiv ⟨unit α R, ⋯⟩ = HopfAlgebras.LForestAlgebra.counit α R

theorem BSeries.LSeries.characterEquiv_symm_counit {α : Type u} {R : Type w} [CommSemiring R] : ↑(characterEquiv.symm (HopfAlgebras.LForestAlgebra.counit α R)) = unit α R

def BSeries.LSeries.exact (α : Type u) (R : Type v) [DivisionSemiring R] : LSeries α R

Exact labelled B-series coefficients, ignoring labels.

Equations

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

@[simp]

theorem BSeries.LSeries.coeff_exact {α : Type u} {R : Type w} [DivisionSemiring R] (τ : LTreeIndex α) : (exact α R).coeff τ = (↑τ.treeFactorial)⁻¹

def BSeries.LSeries.scaledExact (α : Type u) (R : Type v) [DivisionSemiring R] (h : R) : LSeries α R

Exact labelled B-series coefficients at time/step-size h, ignoring labels.

Equations

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

@[simp]

theorem BSeries.LSeries.coeff_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] (h : R) (τ : LTreeIndex α) : (scaledExact α R h).coeff τ = h ^ τ.order * (↑τ.treeFactorial)⁻¹

@[simp]

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

@[simp]

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

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

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

theorem BSeries.LSeries.coeff_exact_tree_graft {α : Type u} {R : Type w} [Field R] (a : α) (φ : HopfAlgebras.LRootedForest α) : (exact α R).coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft a φ)) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.LSeries.coeff_scaledExact_tree_graft {α : Type u} {R : Type w} [Field R] (h : R) (a : α) (φ : HopfAlgebras.LRootedForest α) : (scaledExact α R h).coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft a φ)) = h ^ (1 + φ.order) * (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.LSeries.coeff_exact_tree_branches {α : Type u} {R : Type w} [Field R] (τ : HopfAlgebras.LRootedTree α) : (exact α R).coeff (LTreeIndex.tree τ) = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.LSeries.coeff_scaledExact_tree_branches {α : Type u} {R : Type w} [Field R] (h : R) (τ : HopfAlgebras.LRootedTree α) : (scaledExact α R h).coeff (LTreeIndex.tree τ) = h ^ τ.order * (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.LSeries.coeff_exact_tree_butcherProduct {α : Type u} {R : Type w} [Field R] (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α) : (exact α R).coeff (LTreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.LSeries.coeff_scaledExact_tree_butcherProduct {α : Type u} {R : Type w} [Field R] (h : R) (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α) : (scaledExact α R h).coeff (LTreeIndex.tree (φ.butcherProduct τ)) = h ^ (φ.order + τ.order) * (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

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

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

@[simp]

theorem BSeries.LSeries.forestCoeff_scaledExact_zero {α : Type u} {R : Type w} [Field R] (φ : HopfAlgebras.LRootedForest α) : (scaledExact α R 0).forestCoeff φ = HopfAlgebras.LForestAlgebra.counitCoeff φ

@[simp]

theorem BSeries.LSeries.toCharacter_exact_ofForest {α : Type u} {R : Type w} [Field R] (φ : HopfAlgebras.LRootedForest α) : (exact α R).toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

@[simp]

theorem BSeries.LSeries.toCharacter_scaledExact_ofForest {α : Type u} {R : Type w} [Field R] (h : R) (φ : HopfAlgebras.LRootedForest α) : (scaledExact α R h).toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = h ^ φ.order * (↑φ.treeFactorial)⁻¹

@[simp]

theorem BSeries.LSeries.toCharacter_scaledExact_zero {α : Type u} {R : Type w} [Field R] : (scaledExact α R 0).toCharacter = HopfAlgebras.LForestAlgebra.counit α R

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

Two labelled B-series agree through order n.

Equations

• a.AgreeUpToOrder b n = ∀ (τ : BSeries.LTreeIndex α), τ.order ≤ n → a.coeff τ = b.coeff τ

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

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

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

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

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

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

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

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

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

theorem BSeries.LSeries.agreeUpToOrder_iff_treeCoeff {α : Type u} {R : Type w} {a b : LSeries α R} {n : ℕ} : a.AgreeUpToOrder b n ↔ a.constantCoeff = b.constantCoeff ∧ ∀ (τ : HopfAlgebras.LRootedTree α), τ.order ≤ n → a.coeff (LTreeIndex.tree τ) = b.coeff (LTreeIndex.tree τ)

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

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

theorem BSeries.LSeries.AgreeUpToOrder.toCharacter_ofForest {α : Type u} {R : Type w} [CommSemiring R] {a b : LSeries α R} {n : ℕ} (h : a.AgreeUpToOrder b n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) : a.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = b.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ)

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

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

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

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

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

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

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

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

Coefficient-level order conditions for a labelled B-series.

Equations

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

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

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

theorem BSeries.LSeries.HasOrder.treeCoeff {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} {n : ℕ} (h : a.HasOrder n) {τ : HopfAlgebras.LRootedTree α} (hτ : τ.order ≤ n) : a.coeff (LTreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

theorem BSeries.LSeries.HasOrder.coeff_tree_graft {α : Type u} {R : Type w} [Field R] {a : LSeries α R} {n : ℕ} (h : a.HasOrder n) {x : α} {φ : HopfAlgebras.LRootedForest α} (hφ : 1 + φ.order ≤ n) : a.coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft x φ)) = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

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

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

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

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

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

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

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

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

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

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

theorem BSeries.LSeries.HasOrder.oneNodeCoeff {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} {n : ℕ} (h : a.HasOrder n) (hn : 1 ≤ n) (x : α) : a.coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft x 0)) = 1

theorem BSeries.LSeries.hasOrder_one_iff {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} : a.HasOrder 1 ↔ a.HasUnitConstant ∧ ∀ (x : α), a.coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft x 0)) = 1

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

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

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

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

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

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

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

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

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

theorem BSeries.LSeries.HasOrder.toCharacter_ofForest {α : Type u} {R : Type w} [Field R] {a : LSeries α R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) : a.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

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

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

theorem BSeries.LSeries.HasOrder.coeff_butcherProduct {α : Type u} {R : Type w} [Field R] {a : LSeries α R} {n : ℕ} (h : a.HasOrder n) {φ : HopfAlgebras.LRootedForest α} {τ : HopfAlgebras.LRootedTree α} (horder : φ.order + τ.order ≤ n) : a.coeff (LTreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

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

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

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

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

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

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

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

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

theorem BSeries.LSeries.hasOrder_all_iff_coeff_butcherProduct {α : Type u} {R : Type w} [Field R] {a : LSeries α R} : (∀ (n : ℕ), a.HasOrder n) ↔ a.HasUnitConstant ∧ ∀ (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α), a.coeff (LTreeIndex.tree (φ.butcherProduct τ)) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

def BSeries.LSeries.comapMapLabels {α : Type u} {β : Type v} {R : Type w} (f : α → β) (a : LSeries β R) : LSeries α R

Pull a labelled B-series back along a relabelling map.

Equations

• BSeries.LSeries.comapMapLabels f a τ = a.coeff (BSeries.LTreeIndex.mapLabels f τ)

@[simp]

theorem BSeries.LSeries.coeff_comapMapLabels {α : Type u} {β : Type v} {R : Type w} (f : α → β) (a : LSeries β R) (τ : LTreeIndex α) : (comapMapLabels f a).coeff τ = a.coeff (LTreeIndex.mapLabels f τ)

theorem BSeries.LSeries.forestCoeff_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [CommSemiring R] (f : α → β) (a : LSeries β R) (φ : HopfAlgebras.LRootedForest α) : (comapMapLabels f a).forestCoeff φ = a.forestCoeff (HopfAlgebras.LRootedForest.mapLabels f φ)

theorem BSeries.LSeries.toCharacter_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [CommSemiring R] (f : α → β) (a : LSeries β R) : (comapMapLabels f a).toCharacter = HopfAlgebras.LForestAlgebra.Character.comapMapLabels f a.toCharacter

theorem BSeries.LSeries.hasUnitConstant_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [One R] (f : α → β) {a : LSeries β R} (ha : a.HasUnitConstant) : (comapMapLabels f a).HasUnitConstant

@[simp]

theorem BSeries.LSeries.comapMapLabels_id {α : Type u} {R : Type w} (a : LSeries α R) : comapMapLabels (fun (x : α) => x) a = a

theorem BSeries.LSeries.comapMapLabels_comp {α : Type u} {β : Type v} {γ : Type x} {R : Type w} (g : β → γ) (f : α → β) (a : LSeries γ R) : comapMapLabels f (comapMapLabels g a) = comapMapLabels (g ∘ f) a

@[simp]

theorem BSeries.LSeries.comapMapLabels_unit {α : Type u} {β : Type v} {R : Type w} [Zero R] [One R] (f : α → β) : comapMapLabels f (unit β R) = unit α R

@[simp]

theorem BSeries.LSeries.comapMapLabels_exact {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] (f : α → β) : comapMapLabels f (exact β R) = exact α R

@[simp]

theorem BSeries.LSeries.comapMapLabels_scaledExact {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] (f : α → β) (h : R) : comapMapLabels f (scaledExact β R h) = scaledExact α R h

theorem BSeries.LSeries.agreeUpToOrder_comapMapLabels {α : Type u} {β : Type v} {R : Type w} {a b : LSeries β R} {n : ℕ} (f : α → β) (h : a.AgreeUpToOrder b n) : (comapMapLabels f a).AgreeUpToOrder (comapMapLabels f b) n

theorem BSeries.LSeries.agreeUpToOrder_comapMapLabels_iff_of_surjective {α : Type u} {β : Type v} {R : Type w} {a b : LSeries β R} {n : ℕ} {f : α → β} (hf : Function.Surjective f) : (comapMapLabels f a).AgreeUpToOrder (comapMapLabels f b) n ↔ a.AgreeUpToOrder b n

theorem BSeries.LSeries.comapMapLabels_hasOrder {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] {a : LSeries β R} {n : ℕ} (f : α → β) (h : a.HasOrder n) : (comapMapLabels f a).HasOrder n

theorem BSeries.LSeries.comapMapLabels_hasOrder_iff_of_surjective {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] {a : LSeries β R} {n : ℕ} {f : α → β} (hf : Function.Surjective f) : (comapMapLabels f a).HasOrder n ↔ a.HasOrder n

theorem BSeries.LSeries.agreeUpToOrder_all_comapMapLabels {α : Type u} {β : Type v} {R : Type w} {a b : LSeries β R} (f : α → β) (h : ∀ (n : ℕ), a.AgreeUpToOrder b n) (n : ℕ) : (comapMapLabels f a).AgreeUpToOrder (comapMapLabels f b) n

theorem BSeries.LSeries.agreeUpToOrder_all_comapMapLabels_iff_of_surjective {α : Type u} {β : Type v} {R : Type w} {a b : LSeries β R} {f : α → β} (hf : Function.Surjective f) : (∀ (n : ℕ), (comapMapLabels f a).AgreeUpToOrder (comapMapLabels f b) n) ↔ ∀ (n : ℕ), a.AgreeUpToOrder b n

theorem BSeries.LSeries.comapMapLabels_hasOrder_all {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] {a : LSeries β R} (f : α → β) (h : ∀ (n : ℕ), a.HasOrder n) (n : ℕ) : (comapMapLabels f a).HasOrder n

theorem BSeries.LSeries.comapMapLabels_hasOrder_all_iff_of_surjective {α : Type u} {β : Type v} {R : Type w} [DivisionSemiring R] {a : LSeries β R} {f : α → β} (hf : Function.Surjective f) : (∀ (n : ℕ), (comapMapLabels f a).HasOrder n) ↔ ∀ (n : ℕ), a.HasOrder n

def BSeries.LSeries.comapConstLabel {α : Type u} {R : Type w} (x : α) (a : LSeries α R) : Series R

Restrict a labelled B-series to trees where every vertex has the same label.

Equations

• BSeries.LSeries.comapConstLabel x a τ = a.coeff (BSeries.LTreeIndex.constLabel x τ)

@[simp]

theorem BSeries.LSeries.coeff_comapConstLabel {α : Type u} {R : Type w} (x : α) (a : LSeries α R) (τ : HopfAlgebras.TreeIndex) : (comapConstLabel x a).coeff τ = a.coeff (LTreeIndex.constLabel x τ)

theorem BSeries.LSeries.forestCoeff_comapConstLabel {α : Type u} {R : Type w} [CommSemiring R] (x : α) (a : LSeries α R) (φ : HopfAlgebras.RootedForest) : (comapConstLabel x a).forestCoeff φ = a.forestCoeff (HopfAlgebras.LRootedForest.constLabel x φ)

theorem BSeries.LSeries.toCharacter_comapConstLabel {α : Type u} {R : Type w} [CommSemiring R] (x : α) (a : LSeries α R) : (comapConstLabel x a).toCharacter = HopfAlgebras.LForestAlgebra.Character.comapConstLabel x a.toCharacter

theorem BSeries.LSeries.hasUnitConstant_comapConstLabel {α : Type u} {R : Type w} [One R] (x : α) {a : LSeries α R} (ha : a.HasUnitConstant) : (comapConstLabel x a).HasUnitConstant

@[simp]

theorem BSeries.LSeries.comapConstLabel_unit {α : Type u} {R : Type w} [Zero R] [One R] (x : α) : comapConstLabel x (unit α R) = Series.unit R

@[simp]

theorem BSeries.LSeries.comapConstLabel_exact {α : Type u} {R : Type w} [DivisionSemiring R] (x : α) : comapConstLabel x (exact α R) = Series.exact R

@[simp]

theorem BSeries.LSeries.comapConstLabel_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] (x : α) (h : R) : comapConstLabel x (scaledExact α R h) = Series.scaledExact h

theorem BSeries.LSeries.agreeUpToOrder_comapConstLabel {α : Type u} {R : Type w} {a b : LSeries α R} {n : ℕ} (x : α) (h : a.AgreeUpToOrder b n) : (comapConstLabel x a).AgreeUpToOrder (comapConstLabel x b) n

theorem BSeries.LSeries.comapConstLabel_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} {n : ℕ} (x : α) (h : a.HasOrder n) : (comapConstLabel x a).HasOrder n

theorem BSeries.LSeries.agreeUpToOrder_all_comapConstLabel {α : Type u} {R : Type w} {a b : LSeries α R} (x : α) (h : ∀ (n : ℕ), a.AgreeUpToOrder b n) (n : ℕ) : (comapConstLabel x a).AgreeUpToOrder (comapConstLabel x b) n

theorem BSeries.LSeries.comapConstLabel_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} (x : α) (h : ∀ (n : ℕ), a.HasOrder n) (n : ℕ) : (comapConstLabel x a).HasOrder n

def BSeries.LSeries.comapEraseLabels {α : Type u} {R : Type w} (a : Series R) : LSeries α R

Pull an unlabelled B-series back to labelled trees by forgetting labels.

Equations

• BSeries.LSeries.comapEraseLabels a τ = a.coeff τ.erase

@[simp]

theorem BSeries.LSeries.coeff_comapEraseLabels {α : Type u} {R : Type w} (a : Series R) (τ : LTreeIndex α) : (comapEraseLabels a).coeff τ = a.coeff τ.erase

theorem BSeries.LSeries.forestCoeff_comapEraseLabels {α : Type u} {R : Type w} [CommSemiring R] (a : Series R) (φ : HopfAlgebras.LRootedForest α) : (comapEraseLabels a).forestCoeff φ = a.forestCoeff φ.erase

theorem BSeries.LSeries.toCharacter_comapEraseLabels {α : Type u} {R : Type w} [CommSemiring R] (a : Series R) : (comapEraseLabels a).toCharacter = HopfAlgebras.LForestAlgebra.Character.comapEraseLabels a.toCharacter

theorem BSeries.LSeries.hasUnitConstant_comapEraseLabels {α : Type u} {R : Type w} [One R] {a : Series R} (ha : a.HasUnitConstant) : (comapEraseLabels a).HasUnitConstant

theorem BSeries.LSeries.ofCharacter_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [CommSemiring R] (f : α → β) (χ : HopfAlgebras.LForestAlgebra.Character β R) : ofCharacter (HopfAlgebras.LForestAlgebra.Character.comapMapLabels f χ) = comapMapLabels f (ofCharacter χ)

theorem BSeries.LSeries.ofCharacter_comapEraseLabels {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : ofCharacter (HopfAlgebras.LForestAlgebra.Character.comapEraseLabels χ) = comapEraseLabels (Series.ofCharacter χ)

theorem BSeries.LSeries.ofCharacter_comapConstLabel {α : Type u} {R : Type w} [CommSemiring R] (x : α) (χ : HopfAlgebras.LForestAlgebra.Character α R) : Series.ofCharacter (HopfAlgebras.LForestAlgebra.Character.comapConstLabel x χ) = comapConstLabel x (ofCharacter χ)

theorem BSeries.LSeries.characterEquiv_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [CommSemiring R] (f : α → β) (a : { a : LSeries β R // a.HasUnitConstant }) : characterEquiv ⟨comapMapLabels f ↑a, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.comapMapLabels f (characterEquiv a)

theorem BSeries.LSeries.characterEquiv_comapConstLabel {α : Type u} {R : Type w} [CommSemiring R] (x : α) (a : { a : LSeries α R // a.HasUnitConstant }) : Series.characterEquiv ⟨comapConstLabel x ↑a, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.comapConstLabel x (characterEquiv a)

theorem BSeries.LSeries.characterEquiv_comapEraseLabels {α : Type u} {R : Type w} [CommSemiring R] (a : { a : Series R // a.HasUnitConstant }) : characterEquiv ⟨comapEraseLabels ↑a, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.comapEraseLabels (Series.characterEquiv a)

theorem BSeries.LSeries.characterEquiv_symm_comapMapLabels {α : Type u} {β : Type v} {R : Type w} [CommSemiring R] (f : α → β) (χ : HopfAlgebras.LForestAlgebra.Character β R) : ↑(characterEquiv.symm (HopfAlgebras.LForestAlgebra.Character.comapMapLabels f χ)) = comapMapLabels f ↑(characterEquiv.symm χ)

theorem BSeries.LSeries.characterEquiv_symm_comapConstLabel {α : Type u} {R : Type w} [CommSemiring R] (x : α) (χ : HopfAlgebras.LForestAlgebra.Character α R) : ↑(Series.characterEquiv.symm (HopfAlgebras.LForestAlgebra.Character.comapConstLabel x χ)) = comapConstLabel x ↑(characterEquiv.symm χ)

theorem BSeries.LSeries.characterEquiv_symm_comapEraseLabels {α : Type u} {R : Type w} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : ↑(characterEquiv.symm (HopfAlgebras.LForestAlgebra.Character.comapEraseLabels χ)) = comapEraseLabels ↑(Series.characterEquiv.symm χ)

@[simp]

theorem BSeries.LSeries.comapEraseLabels_unit {α : Type u} {R : Type w} [Zero R] [One R] : comapEraseLabels (Series.unit R) = unit α R

@[simp]

theorem BSeries.LSeries.comapEraseLabels_exact {α : Type u} {R : Type w} [DivisionSemiring R] : comapEraseLabels (Series.exact R) = exact α R

@[simp]

theorem BSeries.LSeries.comapEraseLabels_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] (h : R) : comapEraseLabels (Series.scaledExact h) = scaledExact α R h

theorem BSeries.LSeries.comapEraseLabels_comapMapLabels {α : Type u} {β : Type v} {R : Type w} (f : α → β) (a : Series R) : comapMapLabels f (comapEraseLabels a) = comapEraseLabels a

theorem BSeries.LSeries.comapConstLabel_comapEraseLabels {α : Type u} {R : Type w} (x : α) (a : Series R) : comapConstLabel x (comapEraseLabels a) = a

theorem BSeries.LSeries.comapConstLabel_comapMapLabels {α : Type u} {β : Type v} {R : Type w} (f : α → β) (x : α) (a : LSeries β R) : comapConstLabel x (comapMapLabels f a) = comapConstLabel (f x) a

theorem BSeries.LSeries.agreeUpToOrder_comapEraseLabels {α : Type u} {R : Type w} {a b : Series R} {n : ℕ} (h : a.AgreeUpToOrder b n) : (comapEraseLabels a).AgreeUpToOrder (comapEraseLabels b) n

theorem BSeries.LSeries.agreeUpToOrder_of_comapEraseLabels {α : Type u} {R : Type w} {a b : Series R} {n : ℕ} (x : α) (h : (comapEraseLabels a).AgreeUpToOrder (comapEraseLabels b) n) : a.AgreeUpToOrder b n

theorem BSeries.LSeries.agreeUpToOrder_comapEraseLabels_iff {α : Type u} {R : Type w} [Nonempty α] {a b : Series R} {n : ℕ} : (comapEraseLabels a).AgreeUpToOrder (comapEraseLabels b) n ↔ a.AgreeUpToOrder b n

theorem BSeries.LSeries.comapEraseLabels_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] {a : Series R} {n : ℕ} (h : a.HasOrder n) : (comapEraseLabels a).HasOrder n

theorem BSeries.LSeries.hasOrder_of_comapEraseLabels {α : Type u} {R : Type w} [DivisionSemiring R] {a : Series R} {n : ℕ} (x : α) (h : (comapEraseLabels a).HasOrder n) : a.HasOrder n

theorem BSeries.LSeries.comapEraseLabels_hasOrder_iff {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : Series R} {n : ℕ} : (comapEraseLabels a).HasOrder n ↔ a.HasOrder n

theorem BSeries.LSeries.agreeUpToOrder_all_comapEraseLabels {α : Type u} {R : Type w} {a b : Series R} (h : ∀ (n : ℕ), a.AgreeUpToOrder b n) (n : ℕ) : (comapEraseLabels a).AgreeUpToOrder (comapEraseLabels b) n

theorem BSeries.LSeries.agreeUpToOrder_all_comapEraseLabels_iff {α : Type u} {R : Type w} [Nonempty α] {a b : Series R} : (∀ (n : ℕ), (comapEraseLabels a).AgreeUpToOrder (comapEraseLabels b) n) ↔ ∀ (n : ℕ), a.AgreeUpToOrder b n

theorem BSeries.LSeries.comapEraseLabels_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] {a : Series R} (h : ∀ (n : ℕ), a.HasOrder n) (n : ℕ) : (comapEraseLabels a).HasOrder n

theorem BSeries.LSeries.comapEraseLabels_hasOrder_all_iff {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : Series R} : (∀ (n : ℕ), (comapEraseLabels a).HasOrder n) ↔ ∀ (n : ℕ), a.HasOrder n

def BSeries.LSeries.LabelInvariant {α : Type u} {R : Type w} (a : LSeries α R) : Prop

A labelled B-series whose coefficients only depend on the unlabelled tree.

Equations

• a.LabelInvariant = ∀ (τ σ : BSeries.LTreeIndex α), τ.erase = σ.erase → a.coeff τ = a.coeff σ

theorem BSeries.LSeries.LabelInvariant.coeff_eq {α : Type u} {R : Type w} {a : LSeries α R} (h : a.LabelInvariant) {τ σ : LTreeIndex α} (hτσ : τ.erase = σ.erase) : a.coeff τ = a.coeff σ

theorem BSeries.LSeries.labelInvariant_comapEraseLabels {α : Type u} {R : Type w} (a : Series R) : (comapEraseLabels a).LabelInvariant

theorem BSeries.LSeries.labelInvariant_unit {α : Type u} {R : Type w} [Zero R] [One R] : (unit α R).LabelInvariant

theorem BSeries.LSeries.labelInvariant_exact {α : Type u} {R : Type w} [DivisionSemiring R] : (exact α R).LabelInvariant

theorem BSeries.LSeries.labelInvariant_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] (h : R) : (scaledExact α R h).LabelInvariant

theorem BSeries.LSeries.labelInvariant_zero {α : Type u} {R : Type w} [Zero R] : LabelInvariant 0

theorem BSeries.LSeries.LabelInvariant.add {α : Type u} {R : Type w} [Add R] {a b : LSeries α R} (ha : a.LabelInvariant) (hb : b.LabelInvariant) : (a + b).LabelInvariant

theorem BSeries.LSeries.LabelInvariant.neg {α : Type u} {R : Type w} [Neg R] {a : LSeries α R} (ha : a.LabelInvariant) : (-a).LabelInvariant

theorem BSeries.LSeries.LabelInvariant.sub {α : Type u} {R : Type w} [Sub R] {a b : LSeries α R} (ha : a.LabelInvariant) (hb : b.LabelInvariant) : (a - b).LabelInvariant

theorem BSeries.LSeries.LabelInvariant.smul {α : Type u} {R : Type w} {S : Type y} [SMul S R] {a : LSeries α R} (c : S) (ha : a.LabelInvariant) : (c • a).LabelInvariant

theorem BSeries.LSeries.LabelInvariant.comapMapLabels {α : Type u} {β : Type v} {R : Type w} {a : LSeries β R} (h : a.LabelInvariant) (f : α → β) : (LSeries.comapMapLabels f a).LabelInvariant

theorem BSeries.LSeries.LabelInvariant.comapConstLabel_eq {α : Type u} {R : Type w} {a : LSeries α R} (h : a.LabelInvariant) (x y : α) : comapConstLabel x a = comapConstLabel y a

theorem BSeries.LSeries.LabelInvariant.comapEraseLabels_comapConstLabel {α : Type u} {R : Type w} {a : LSeries α R} (h : a.LabelInvariant) (x : α) : comapEraseLabels (comapConstLabel x a) = a

noncomputable def BSeries.LSeries.labelInvariantEquiv {α : Type u} {R : Type w} [Nonempty α] : Series R ≃ { a : LSeries α R // a.LabelInvariant }

Unlabelled series are equivalent to labelled series whose coefficients ignore labels.

Equations

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

@[simp]

theorem BSeries.LSeries.labelInvariantEquiv_apply {α : Type u} {R : Type w} [Nonempty α] (a : Series R) : ↑(labelInvariantEquiv a) = comapEraseLabels a

@[simp]

theorem BSeries.LSeries.labelInvariantEquiv_symm_apply {α : Type u} {R : Type w} [Nonempty α] (a : { a : LSeries α R // a.LabelInvariant }) : labelInvariantEquiv.symm a = comapConstLabel (Classical.choice ⋯) ↑a

theorem BSeries.LSeries.labelInvariantEquiv_unit {α : Type u} {R : Type w} [Zero R] [One R] [Nonempty α] : labelInvariantEquiv (Series.unit R) = ⟨unit α R, ⋯⟩

theorem BSeries.LSeries.labelInvariantEquiv_symm_unit {α : Type u} {R : Type w} [Zero R] [One R] [Nonempty α] : labelInvariantEquiv.symm ⟨unit α R, ⋯⟩ = Series.unit R

theorem BSeries.LSeries.labelInvariant_iff_exists_comapEraseLabels {α : Type u} {R : Type w} [Nonempty α] (a : LSeries α R) : a.LabelInvariant ↔ ∃ (b : Series R), comapEraseLabels b = a

theorem BSeries.LSeries.labelInvariantEquiv_hasUnitConstant {α : Type u} {R : Type w} [One R] [Nonempty α] {a : Series R} : (↑(labelInvariantEquiv a)).HasUnitConstant ↔ a.HasUnitConstant

theorem BSeries.LSeries.labelInvariantEquiv_symm_hasUnitConstant {α : Type u} {R : Type w} [One R] [Nonempty α] {a : { a : LSeries α R // a.LabelInvariant }} : (labelInvariantEquiv.symm a).HasUnitConstant ↔ (↑a).HasUnitConstant

noncomputable def BSeries.LSeries.labelInvariantUnitEquiv {α : Type u} {R : Type w} [One R] [Nonempty α] : { a : Series R // a.HasUnitConstant } ≃ { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }

Unit-constant unlabelled series are equivalent to unit-constant label-invariant series.

Equations

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

@[simp]

theorem BSeries.LSeries.labelInvariantUnitEquiv_apply {α : Type u} {R : Type w} [One R] [Nonempty α] (a : { a : Series R // a.HasUnitConstant }) : ↑(labelInvariantUnitEquiv a) = comapEraseLabels ↑a

@[simp]

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_apply {α : Type u} {R : Type w} [One R] [Nonempty α] (a : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }) : ↑(labelInvariantUnitEquiv.symm a) = comapConstLabel (Classical.choice ⋯) ↑a

theorem BSeries.LSeries.labelInvariantUnitEquiv_unit {α : Type u} {R : Type w} [Zero R] [One R] [Nonempty α] : labelInvariantUnitEquiv ⟨Series.unit R, ⋯⟩ = ⟨unit α R, ⋯⟩

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_unit {α : Type u} {R : Type w} [Zero R] [One R] [Nonempty α] : ↑(labelInvariantUnitEquiv.symm ⟨unit α R, ⋯⟩) = Series.unit R

theorem BSeries.LSeries.LabelInvariant.toCharacter {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] {a : LSeries α R} (h : a.LabelInvariant) : a.toCharacter.LabelInvariant

theorem BSeries.LSeries.labelInvariant_of_toCharacter {α : Type u} {R : Type w} [CommSemiring R] {a : LSeries α R} (h : a.toCharacter.LabelInvariant) : a.LabelInvariant

theorem BSeries.LSeries.labelInvariant_iff_toCharacter_labelInvariant {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] {a : LSeries α R} : a.LabelInvariant ↔ a.toCharacter.LabelInvariant

theorem BSeries.LSeries.characterEquiv_labelInvariant_iff {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] (a : { a : LSeries α R // a.HasUnitConstant }) : (characterEquiv a).LabelInvariant ↔ (↑a).LabelInvariant

noncomputable def BSeries.LSeries.labelInvariantCharacterEquiv {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant } ≃ { χ : HopfAlgebras.LForestAlgebra.Character α R // χ.LabelInvariant }

Unit-constant label-invariant series are equivalent to label-invariant characters.

Equations

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

@[simp]

theorem BSeries.LSeries.labelInvariantCharacterEquiv_apply {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] (a : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }) : ↑(labelInvariantCharacterEquiv a) = characterEquiv ⟨↑a, ⋯⟩

@[simp]

theorem BSeries.LSeries.labelInvariantCharacterEquiv_symm_apply {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] (χ : { χ : HopfAlgebras.LForestAlgebra.Character α R // χ.LabelInvariant }) : ↑(labelInvariantCharacterEquiv.symm χ) = ↑(characterEquiv.symm ↑χ)

theorem BSeries.LSeries.labelInvariantCharacterEquiv_labelInvariantUnitEquiv {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] (a : { a : Series R // a.HasUnitConstant }) : labelInvariantCharacterEquiv (labelInvariantUnitEquiv a) = HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv (Series.characterEquiv a)

theorem BSeries.LSeries.labelInvariantCharacterEquiv_unit {α : Type u} {R : Type w} [CommSemiring R] [Nonempty α] : labelInvariantCharacterEquiv ⟨unit α R, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv (Series.characterEquiv ⟨Series.unit R, ⋯⟩)

theorem BSeries.LSeries.labelInvariantUnitEquiv_exact {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] : labelInvariantUnitEquiv ⟨Series.exact R, ⋯⟩ = ⟨exact α R, ⋯⟩

theorem BSeries.LSeries.labelInvariantUnitEquiv_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] (h : R) : labelInvariantUnitEquiv ⟨Series.scaledExact h, ⋯⟩ = ⟨scaledExact α R h, ⋯⟩

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_exact {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] : ↑(labelInvariantUnitEquiv.symm ⟨exact α R, ⋯⟩) = Series.exact R

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_scaledExact {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] (h : R) : ↑(labelInvariantUnitEquiv.symm ⟨scaledExact α R h, ⋯⟩) = Series.scaledExact h

theorem BSeries.LSeries.labelInvariantUnitEquiv_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : Series R // a.HasUnitConstant }} {n : ℕ} : (↑(labelInvariantUnitEquiv a)).HasOrder n ↔ (↑a).HasOrder n

theorem BSeries.LSeries.labelInvariantUnitEquiv_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : Series R // a.HasUnitConstant }} : (∀ (n : ℕ), (↑(labelInvariantUnitEquiv a)).HasOrder n) ↔ ∀ (n : ℕ), (↑a).HasOrder n

theorem BSeries.LSeries.labelInvariantCharacterEquiv_exact {α : Type u} {R : Type w} [Field R] [Nonempty α] : labelInvariantCharacterEquiv ⟨exact α R, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv (Series.characterEquiv ⟨Series.exact R, ⋯⟩)

theorem BSeries.LSeries.labelInvariantCharacterEquiv_scaledExact {α : Type u} {R : Type w} [Field R] [Nonempty α] (h : R) : labelInvariantCharacterEquiv ⟨scaledExact α R h, ⋯⟩ = HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv (Series.characterEquiv ⟨Series.scaledExact h, ⋯⟩)

theorem BSeries.LSeries.labelInvariantCharacterEquiv_hasOrder_all_iff_exact {α : Type u} {R : Type w} [Field R] [Nonempty α] (a : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }) : (∀ (n : ℕ), (↑a).HasOrder n) ↔ labelInvariantCharacterEquiv a = labelInvariantCharacterEquiv ⟨exact α R, ⋯⟩

theorem BSeries.LSeries.LabelInvariant.agreeUpToOrder_iff_comapConstLabel {α : Type u} {R : Type w} {a b : LSeries α R} {n : ℕ} (ha : a.LabelInvariant) (hb : b.LabelInvariant) (x : α) : a.AgreeUpToOrder b n ↔ (comapConstLabel x a).AgreeUpToOrder (comapConstLabel x b) n

theorem BSeries.LSeries.LabelInvariant.hasOrder_iff_comapConstLabel {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} {n : ℕ} (ha : a.LabelInvariant) (x : α) : a.HasOrder n ↔ (comapConstLabel x a).HasOrder n

theorem BSeries.LSeries.LabelInvariant.agreeUpToOrder_all_iff_comapConstLabel {α : Type u} {R : Type w} {a b : LSeries α R} (ha : a.LabelInvariant) (hb : b.LabelInvariant) (x : α) : (∀ (n : ℕ), a.AgreeUpToOrder b n) ↔ ∀ (n : ℕ), (comapConstLabel x a).AgreeUpToOrder (comapConstLabel x b) n

theorem BSeries.LSeries.LabelInvariant.hasOrder_all_iff_comapConstLabel {α : Type u} {R : Type w} [DivisionSemiring R] {a : LSeries α R} (ha : a.LabelInvariant) (x : α) : (∀ (n : ℕ), a.HasOrder n) ↔ ∀ (n : ℕ), (comapConstLabel x a).HasOrder n

theorem BSeries.LSeries.labelInvariantUnitEquiv_agreeUpToOrder {α : Type u} {R : Type w} [One R] [Nonempty α] {a b : { a : Series R // a.HasUnitConstant }} {n : ℕ} : (↑(labelInvariantUnitEquiv a)).AgreeUpToOrder (↑(labelInvariantUnitEquiv b)) n ↔ (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_agreeUpToOrder {α : Type u} {R : Type w} [One R] [Nonempty α] {a b : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }} {n : ℕ} : (↑(labelInvariantUnitEquiv.symm a)).AgreeUpToOrder (↑(labelInvariantUnitEquiv.symm b)) n ↔ (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }} {n : ℕ} : (↑(labelInvariantUnitEquiv.symm a)).HasOrder n ↔ (↑a).HasOrder n

theorem BSeries.LSeries.labelInvariantUnitEquiv_agreeUpToOrder_all {α : Type u} {R : Type w} [One R] [Nonempty α] {a b : { a : Series R // a.HasUnitConstant }} : (∀ (n : ℕ), (↑(labelInvariantUnitEquiv a)).AgreeUpToOrder (↑(labelInvariantUnitEquiv b)) n) ↔ ∀ (n : ℕ), (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_agreeUpToOrder_all {α : Type u} {R : Type w} [One R] [Nonempty α] {a b : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }} : (∀ (n : ℕ), (↑(labelInvariantUnitEquiv.symm a)).AgreeUpToOrder (↑(labelInvariantUnitEquiv.symm b)) n) ↔ ∀ (n : ℕ), (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantUnitEquiv_symm_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : LSeries α R // a.HasUnitConstant ∧ a.LabelInvariant }} : (∀ (n : ℕ), (↑(labelInvariantUnitEquiv.symm a)).HasOrder n) ↔ ∀ (n : ℕ), (↑a).HasOrder n

theorem BSeries.LSeries.labelInvariantEquiv_agreeUpToOrder {α : Type u} {R : Type w} [Nonempty α] {a b : Series R} {n : ℕ} : (↑(labelInvariantEquiv a)).AgreeUpToOrder (↑(labelInvariantEquiv b)) n ↔ a.AgreeUpToOrder b n

theorem BSeries.LSeries.labelInvariantEquiv_symm_agreeUpToOrder {α : Type u} {R : Type w} [Nonempty α] {a b : { a : LSeries α R // a.LabelInvariant }} {n : ℕ} : (labelInvariantEquiv.symm a).AgreeUpToOrder (labelInvariantEquiv.symm b) n ↔ (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantEquiv_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : Series R} {n : ℕ} : (↑(labelInvariantEquiv a)).HasOrder n ↔ a.HasOrder n

theorem BSeries.LSeries.labelInvariantEquiv_symm_hasOrder {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : LSeries α R // a.LabelInvariant }} {n : ℕ} : (labelInvariantEquiv.symm a).HasOrder n ↔ (↑a).HasOrder n

theorem BSeries.LSeries.labelInvariantEquiv_agreeUpToOrder_all {α : Type u} {R : Type w} [Nonempty α] {a b : Series R} : (∀ (n : ℕ), (↑(labelInvariantEquiv a)).AgreeUpToOrder (↑(labelInvariantEquiv b)) n) ↔ ∀ (n : ℕ), a.AgreeUpToOrder b n

theorem BSeries.LSeries.labelInvariantEquiv_symm_agreeUpToOrder_all {α : Type u} {R : Type w} [Nonempty α] {a b : { a : LSeries α R // a.LabelInvariant }} : (∀ (n : ℕ), (labelInvariantEquiv.symm a).AgreeUpToOrder (labelInvariantEquiv.symm b) n) ↔ ∀ (n : ℕ), (↑a).AgreeUpToOrder (↑b) n

theorem BSeries.LSeries.labelInvariantEquiv_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : Series R} : (∀ (n : ℕ), (↑(labelInvariantEquiv a)).HasOrder n) ↔ ∀ (n : ℕ), a.HasOrder n

theorem BSeries.LSeries.labelInvariantEquiv_symm_hasOrder_all {α : Type u} {R : Type w} [DivisionSemiring R] [Nonempty α] {a : { a : LSeries α R // a.LabelInvariant }} : (∀ (n : ℕ), (labelInvariantEquiv.symm a).HasOrder n) ↔ ∀ (n : ℕ), (↑a).HasOrder n