Lie–Butcher series

Following Munthe-Kaas–Wright (arXiv:math/0603023, Section 2), a Lie series on a manifold is a formal sum LS(α) = Σ_{ω ∈ OF} h^{|ω|} α(ω) F(ω) over ordered forests, determined by its coefficient family α. We work at the coefficient level: an LSSeries is a function on ordered (planar) forests.

Two classes are distinguished by their behaviour under the shuffle product:

• exponential (group-like) series, the shuffle characters — these represent flows of Lie group integrators and form a group under the Grossman–Larson convolution (PlanarForest.mkwConvolution);
• logarithmic (algebra-like) series, which represent vector fields; by Ree's criterion these are the functionals vanishing on the empty forest and on all shuffle products of non-empty forests. A logarithmic series is the non-commutative generalization of a B-series, called a Lie–Butcher series.

As verification we check the paper's example: the commutator τ₁τ₂ - τ₂τ₁ of two trees is logarithmic, as is any single tree.

@[reducible, inline]

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

The coefficient family of a Lie series on a manifold: one coefficient per ordered forest (arXiv:math/0603023, eq. (2.4)).

Equations

• BSeries.LSSeries R = (HopfAlgebras.PlanarForest → R)

def BSeries.LSSeries.IsExponential {R : Type u} [Semiring R] (α : LSSeries R) : Prop

An LS-series is exponential (group-like) if its coefficients form a shuffle character; these represent flows, and Lie group integrators are exactly the exponential series (arXiv:math/0603023, Section 2).

Equations

• α.IsExponential = HopfAlgebras.PlanarForest.IsShuffleCharacter α

def BSeries.LSSeries.IsLieButcher {R : Type u} [Semiring R] (α : LSSeries R) : Prop

An LS-series is logarithmic (algebra-like), i.e. a Lie–Butcher series, if it vanishes on the empty forest and on all shuffle products of non-empty forests (Ree's shuffle criterion for lying in the free Lie algebra; arXiv:math/0603023, Section 2).

Equations

• α.IsLieButcher = (α [] = 0 ∧ ∀ (ω₁ ω₂ : HopfAlgebras.PlanarForest), ω₁ ≠ [] → ω₂ ≠ [] → (List.map α (HopfAlgebras.Word.shuffle ω₁ ω₂)).sum = 0)

def BSeries.LSSeries.compose {R : Type u} [Semiring R] (α β : LSSeries R) : LSSeries R

Composition of LS-series: the Grossman–Larson convolution dual to the MKW coproduct (arXiv:math/0603023, Section 3).

Equations

• α.compose β = HopfAlgebras.PlanarForest.mkwConvolution α β

theorem BSeries.LSSeries.IsExponential.compose {R : Type u} [CommSemiring R] {α β : LSSeries R} (hα : α.IsExponential) (hβ : β.IsExponential) : (α.compose β).IsExponential

The composition of exponential series is exponential: Lie group integrators are closed under composition.

def BSeries.LSSeries.singleTree {R : Type u} [Zero R] [One R] [DecidableEq HopfAlgebras.PlanarForest] (τ : HopfAlgebras.PlanarTree) : LSSeries R

The single-tree series δ_τ.

Equations

• BSeries.LSSeries.singleTree τ ω = if ω = [τ] then 1 else 0

def BSeries.LSSeries.commutator {R : Type u} [AddGroup R] [One R] [DecidableEq HopfAlgebras.PlanarForest] (τ₁ τ₂ : HopfAlgebras.PlanarTree) : LSSeries R

The commutator series τ₁τ₂ - τ₂τ₁ of two trees (arXiv:math/0603023, Section 2).

Equations

• BSeries.LSSeries.commutator τ₁ τ₂ ω = (if ω = [τ₁, τ₂] then 1 else 0) - if ω = [τ₂, τ₁] then 1 else 0

theorem BSeries.LSSeries.isLieButcher_singleTree {R : Type u} [DecidableEq HopfAlgebras.PlanarForest] [Semiring R] (τ : HopfAlgebras.PlanarTree) : (singleTree τ).IsLieButcher

A single tree is a Lie–Butcher series: any shuffle of non-empty forests has at least two trees.

theorem BSeries.LSSeries.isLieButcher_commutator {R : Type u} [DecidableEq HopfAlgebras.PlanarForest] [Ring R] (τ₁ τ₂ : HopfAlgebras.PlanarTree) : (commutator τ₁ τ₂).IsLieButcher

The commutator of two trees is a Lie–Butcher series (arXiv:math/0603023, Section 2): τ₁τ₂ - τ₂τ₁ represents the commutator of two vector fields, and its shuffle sums cancel in pairs.

def BSeries.LSSeries.exactFlow [DecidableEq HopfAlgebras.PlanarTree] (R : Type u) [DivisionRing R] : LSSeries R

The exact flow as a Lie series (arXiv:math/0603023, Section 2): the t = 1 flow of a vector field f = F(•) pulls back functions by the operator exponential Exp(f) = Σ_j f^j / j!, a Lie series supported on the concatenation powers • ⋯ • of the single-node tree with coefficients 1/j!.

Equations

• BSeries.LSSeries.exactFlow R ω = if ∀ t ∈ ω, t = HopfAlgebras.PTree.bullet then (↑(List.length ω).factorial)⁻¹ else 0

theorem BSeries.LSSeries.isExponential_exactFlow [DecidableEq HopfAlgebras.PlanarTree] (R : Type u) [Field R] [CharZero R] : (exactFlow R).IsExponential

The exact flow is exponential (group-like) (arXiv:math/0603023, Section 2): its coefficients form a shuffle character, by the binomial identity C(a+b,a)/(a+b)! = 1/a! ⋅ 1/b!.