The signature of a linear path

The signature of the linear segment with increment v : α → R has word coefficients (∏ v(wᵢ)) / |w|! — the tensor exponential of the increment. It is group-like: the shuffle identity reduces to the counting identity |shuffle u w| = (|u|+|w|).choose |u| together with the factorial identity choose · |u|! · |w|! = (|u|+|w|)!.

theorem RoughPaths.list_range_map_sum {M : Type u_1} [AddCommMonoid M] (n : ℕ) (F : ℕ → M) : (List.map F (List.range n)).sum = ∑ k ∈ Finset.range n, F k

Summing a function over List.range is a Finset.range sum.

theorem RoughPaths.div_factorial_mul_div_factorial {R : Type v} [Field R] [CharZero R] {n k : ℕ} (hk : k ≤ n) (x y : R) : x / ↑k.factorial * (y / ↑(n - k).factorial) = x * y * (↑(n.choose k) / ↑n.factorial)

1/(k!·(n-k)!) regrouped through the binomial coefficient.

theorem RoughPaths.sum_pow_div_factorial {R : Type v} [Field R] (a b : R) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), a ^ k * b ^ (n - k) * (↑(n.choose k) / ↑n.factorial) = (a + b) ^ n / ↑n.factorial

The exponential binomial sum: Σₖ aᵏ·b^{n-k}·C(n,k)/n! = (a+b)ⁿ/n!.

theorem RoughPaths.Word.splits_map_length_fst {α : Type u} (w : List α) : List.map (fun (p : List α × List α) => p.1.length) (HopfAlgebras.Word.splits w) = List.range (w.length + 1)

The prefix lengths of the splits of w are 0, 1, …, |w| in order.

theorem RoughPaths.Word.sum_splits_length_fst {α : Type u} {M : Type u_1} [AddCommMonoid M] (w : List α) (F : ℕ → M) : (List.map (fun (p : List α × List α) => F p.1.length) (HopfAlgebras.Word.splits w)).sum = ∑ k ∈ Finset.range (w.length + 1), F k

A sum over the splits of w that depends only on the prefix length is a sum over Finset.range (|w| + 1).

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

The signature of a linear path with increment v: the tensor exponential w ↦ (∏ᵢ v(wᵢ)) / |w|!.

Equations

• RoughPaths.Word.linearSignature v w = (List.map v w).prod / ↑w.length.factorial

@[simp]

theorem RoughPaths.Word.linearSignature_coeff {α : Type u} {R : Type v} [Field R] (v : α → R) (w : List α) : coeff (linearSignature v) w = (List.map v w).prod / ↑w.length.factorial

@[simp]

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

theorem RoughPaths.Word.shuffleCoeff_linearSignature {α : Type u} {R : Type v} [Field R] (v : α → R) (u w : List α) : shuffleCoeff (linearSignature v) u w = ↑((u.length + w.length).choose u.length) * ((List.map v (u ++ w)).prod / ↑(u.length + w.length).factorial)

The shuffle sum of a linear signature collapses to a binomial multiple: every shuffle of u and w is a permutation of u ++ w, so all summands agree.

theorem RoughPaths.Word.isGroupLike_linearSignature {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) : IsGroupLike (linearSignature v)

The linear signature is group-like (its coefficients satisfy the shuffle identity).

The semigroup law and inverses

@[simp]

theorem RoughPaths.Word.linearSignature_zero {α : Type u} {R : Type v} [Field R] : linearSignature 0 = unit α R

@[simp]

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

@[simp]

theorem RoughPaths.Word.linearSignature_pair {α : Type u} {R : Type v} [Field R] (v : α → R) (x y : α) : linearSignature v [x, y] = v x * v y / 2

theorem RoughPaths.Word.tensorProduct_linearSignature_smul {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) (a b : R) : tensorProduct (linearSignature (a • v)) (linearSignature (b • v)) = linearSignature ((a + b) • v)

Semigroup law for linear signatures: collinear segments concatenate additively, S(a·v) ⊗ S(b·v) = S((a+b)·v) — the binomial identity for the tensor exponential.

theorem RoughPaths.Word.tensorProduct_linearSignature_neg {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) : tensorProduct (linearSignature v) (linearSignature (-v)) = unit α R

Inverse of a linear signature: the reversed segment.

theorem RoughPaths.Word.tensorProduct_linearSignature_neg' {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) : tensorProduct (linearSignature (-v)) (linearSignature v) = unit α R