Lie group integrators as discrete planarly branched rough paths

The bridge between Lie–Butcher series and planarly branched rough paths (RoughPaths.PlanarBranchedRoughPath): the discrete flow of a Lie group integrator — the convolution powers of its exponential LS-series — has shuffle-character increments satisfying Chen's identity for the Grossman–Larson convolution on ordered times. These are exactly the defining fields of a planarly branched rough path, sampled along a mesh.

noncomputable def BSeries.LSSeries.pow {R : Type u} [CommSemiring R] (α : LSSeries R) : ℕ → LSSeries R

Convolution powers of an LS-series: the discrete flow of the integrator.

Equations

• α.pow 0 = HopfAlgebras.PlanarForestAlgebra.counitCoeff
• α.pow n.succ = (α.pow n).compose α

@[simp]

theorem BSeries.LSSeries.pow_zero {R : Type u} [CommSemiring R] (α : LSSeries R) : α.pow 0 = HopfAlgebras.PlanarForestAlgebra.counitCoeff

theorem BSeries.LSSeries.pow_succ {R : Type u} [CommSemiring R] (α : LSSeries R) (n : ℕ) : α.pow (n + 1) = (α.pow n).compose α

theorem BSeries.LSSeries.pow_isExponential {R : Type u} [CommSemiring R] {α : LSSeries R} (hα : α.IsExponential) (n : ℕ) : (α.pow n).IsExponential

Convolution powers of an exponential series are exponential: every step of the discrete flow is a Lie group element.

theorem BSeries.LSSeries.pow_add {R : Type u} [CommSemiring R] (α : LSSeries R) (a b : ℕ) : α.pow (a + b) = (α.pow a).compose (α.pow b)

The discrete flow property: powers add under composition.