Piecewise-linear signatures and Chen's theorem

Group-likeness is closed under the tensor (Chen) product — via the bialgebra keystone Word.shuffle_splits_perm from HopfAlgebras.Words.SplitShuffle — giving the piecewise-linear signature, Chen's theorem for concatenation, and the signature monoid.

Group-likeness of the tensor product

theorem RoughPaths.Word.sum_map_flatMap {R : Type v} {β γ : Type u} [AddCommMonoid R] (l : List β) (f : β → List γ) (g : γ → R) : (List.map g (List.flatMap f l)).sum = (List.map (fun (x : β) => (List.map g (f x)).sum) l).sum

theorem RoughPaths.Word.IsGroupLike.tensorProduct {α : Type u} {R : Type v} [CommSemiring R] {a b : List α → R} (ha : IsGroupLike a) (hb : IsGroupLike b) : IsGroupLike (Word.tensorProduct a b)

The tensor (concatenation) product of group-like series is group-like — the summed form of shuffle–deconcatenation compatibility.

Piecewise-linear signatures and Chen's theorem

def RoughPaths.Word.piecewiseLinearSignature {α : Type u} {R : Type v} [Field R] (segs : List (α → R)) : List α → R

The signature of a piecewise-linear path: the ordered tensor product of the segments' exponentials.

Equations

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

@[simp]

theorem RoughPaths.Word.piecewiseLinearSignature_nil {α : Type u} {R : Type v} [Field R] : piecewiseLinearSignature [] = unit α R

theorem RoughPaths.Word.piecewiseLinearSignature_append {α : Type u} {R : Type v} [Field R] (xs ys : List (α → R)) : piecewiseLinearSignature (xs ++ ys) = tensorProduct (piecewiseLinearSignature xs) (piecewiseLinearSignature ys)

Chen's concatenation theorem for piecewise-linear paths: the signature of a concatenation is the tensor product of the signatures.

theorem RoughPaths.Word.isGroupLike_piecewiseLinearSignature {α : Type u} {R : Type v} [Field R] [CharZero R] (segs : List (α → R)) : IsGroupLike (piecewiseLinearSignature segs)

The signature of a piecewise-linear path is group-like.

@[simp]

theorem RoughPaths.Word.piecewiseLinearSignature_singleton {α : Type u} {R : Type v} [Field R] (v : α → R) : piecewiseLinearSignature [v] = linearSignature v

The signature of a single segment.

theorem RoughPaths.Word.piecewiseLinearSignature_reverse_neg {α : Type u} {R : Type v} [Field R] [CharZero R] (segs : List (α → R)) : tensorProduct (piecewiseLinearSignature segs) (piecewiseLinearSignature (List.map (fun (s : α → R) => -s) segs.reverse)) = unit α R

Group inverse of a piecewise-linear signature: running the path backwards — reversed, negated segments — inverts the signature. Together with piecewiseLinearSignature_append (Chen), the piecewise-linear signatures form a group, not just a monoid.

noncomputable def RoughPaths.Signature.ofPiecewiseLinear {α : Type u} {R : Type v} [Field R] [CharZero R] (segs : List (α → R)) : Signature α R

The bundled signature of a piecewise-linear path.

Equations

• RoughPaths.Signature.ofPiecewiseLinear segs = ⟨RoughPaths.Word.piecewiseLinearSignature segs, ⋯⟩

theorem RoughPaths.Signature.ofPiecewiseLinear_append {α : Type u} {R : Type v} [Field R] [CharZero R] (xs ys : List (α → R)) : ofPiecewiseLinear (xs ++ ys) = ofPiecewiseLinear xs * ofPiecewiseLinear ys

Chen's theorem, bundled: concatenation of paths multiplies signatures.