Word Signatures

This file defines the word-indexed algebraic signature data used in rough path theory. It covers the shuffle identity for group-like signatures and finite degree truncations.

Main definitions

• raw word series List α → R - formal coefficient families indexed by words
• Word.comapMapLetters - relabel word-indexed series by mapping letters
• Word.shuffleCoeff - finite shuffle sum of coefficients
• Word.IsGroupLike - the shuffle identity for signatures
• Word.tensorProduct - concatenation product of signature series
• Word.Truncation - coefficients restricted to words of length at most n
• Word.SatisfiesShuffleUpToDegree - finite-degree shuffle identity
• Signature - bundled group-like signature series

References

• Terry Lyons, Michael Caruana, Thierry Levy, Differential Equations Driven by Rough Paths
• Peter Friz, Nicolas Victoir, Multidimensional Stochastic Processes as Rough Paths

def RoughPaths.Word.coeff {α : Type u} {R : Type w} (a : List α → R) (w : List α) : R

The coefficient of a word in a formal signature series.

Equations

• RoughPaths.Word.coeff a w = a w

@[simp]

theorem RoughPaths.Word.coeff_apply {α : Type u} {R : Type w} (a : List α → R) (w : List α) : coeff a w = a w

theorem RoughPaths.Word.ext {α : Type u} {R : Type w} {a b : List α → R} (h : ∀ (w : List α), coeff a w = coeff b w) : a = b

theorem RoughPaths.Word.ext_iff {α : Type u} {R : Type w} {a b : List α → R} : a = b ↔ ∀ (w : List α), coeff a w = coeff b w

def RoughPaths.Word.emptyCoeff {α : Type u} {R : Type w} (a : List α → R) : R

The coefficient of the empty word.

Equations

• RoughPaths.Word.emptyCoeff a = RoughPaths.Word.coeff a []

@[simp]

theorem RoughPaths.Word.coeff_nil {α : Type u} {R : Type w} (a : List α → R) : coeff a [] = emptyCoeff a

def RoughPaths.Word.HasUnitEmpty {α : Type u} {R : Type w} [One R] (a : List α → R) : Prop

Unit empty-word coefficient condition.

Equations

• RoughPaths.Word.HasUnitEmpty a = (RoughPaths.Word.emptyCoeff a = 1)

theorem RoughPaths.Word.HasUnitEmpty.coeff_nil {α : Type u} {R : Type w} [One R] {a : List α → R} (h : HasUnitEmpty a) : coeff a [] = 1

def RoughPaths.Word.comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} (f : γ → δ) (a : List δ → R) : List γ → R

Relabel a word-indexed series.

Equations

• RoughPaths.Word.comapMapLetters f a w = a (List.map f w)

@[simp]

theorem RoughPaths.Word.coeff_comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} (f : γ → δ) (a : List δ → R) (w : List γ) : coeff (comapMapLetters f a) w = coeff a (List.map f w)

theorem RoughPaths.Word.HasUnitEmpty.comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} [One R] {a : List δ → R} (h : HasUnitEmpty a) (f : γ → δ) : HasUnitEmpty (Word.comapMapLetters f a)

@[simp]

theorem RoughPaths.Word.comapMapLetters_id {α : Type u} {R : Type w} (a : List α → R) : comapMapLetters id a = a

theorem RoughPaths.Word.comapMapLetters_comp {R : Type w} {γ : Type u} {δ : Type v} {ε : Type z} (f : γ → δ) (g : δ → ε) (a : List ε → R) : comapMapLetters f (comapMapLetters g a) = comapMapLetters (g ∘ f) a

def RoughPaths.Word.unit (α : Type u) (R : Type v) [Zero R] [One R] : List α → R

The unit signature series.

Equations

• RoughPaths.Word.unit α R [] = 1
• RoughPaths.Word.unit α R (head :: tail) = 0

@[simp]

theorem RoughPaths.Word.coeff_unit_nil {α : Type u} {R : Type w} [Zero R] [One R] : coeff (unit α R) [] = 1

@[simp]

theorem RoughPaths.Word.coeff_unit_cons {α : Type u} {R : Type w} [Zero R] [One R] (x : α) (w : List α) : coeff (unit α R) (x :: w) = 0

theorem RoughPaths.Word.unit_hasUnitEmpty {α : Type u} {R : Type w} [Zero R] [One R] : HasUnitEmpty (unit α R)

@[simp]

theorem RoughPaths.Word.comapMapLetters_unit {R : Type w} {γ : Type u} {δ : Type v} [Zero R] [One R] (f : γ → δ) : comapMapLetters f (unit δ R) = unit γ R

def RoughPaths.Word.shuffleCoeff {α : Type u} {R : Type w} [AddMonoid R] (a : List α → R) (u v : List α) : R

Sum of coefficients over all shuffles of two words.

Equations

• RoughPaths.Word.shuffleCoeff a u v = (List.map a (HopfAlgebras.Word.shuffle u v)).sum

@[simp]

theorem RoughPaths.Word.shuffleCoeff_nil_left {α : Type u} {R : Type w} [AddMonoid R] (a : List α → R) (v : List α) : shuffleCoeff a [] v = coeff a v

@[simp]

theorem RoughPaths.Word.shuffleCoeff_nil_right {α : Type u} {R : Type w} [AddMonoid R] (a : List α → R) (u : List α) : shuffleCoeff a u [] = coeff a u

theorem RoughPaths.Word.shuffleCoeff_comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} [AddMonoid R] (f : γ → δ) (a : List δ → R) (u v : List γ) : shuffleCoeff (comapMapLetters f a) u v = shuffleCoeff a (List.map f u) (List.map f v)

theorem RoughPaths.Word.shuffleCoeff_unit {α : Type u} {R : Type w} [Semiring R] (u v : List α) : shuffleCoeff (unit α R) u v = unit α R u * unit α R v

def RoughPaths.Word.IsGroupLike {α : Type u} {R : Type w} [Semiring R] (a : List α → R) : Prop

A signature series satisfying the shuffle identity.

Equations

• RoughPaths.Word.IsGroupLike a = (RoughPaths.Word.coeff a [] = 1 ∧ ∀ (u v : List α), RoughPaths.Word.coeff a u * RoughPaths.Word.coeff a v = RoughPaths.Word.shuffleCoeff a u v)

theorem RoughPaths.Word.IsGroupLike.coeff_nil {α : Type u} {R : Type w} [Semiring R] {a : List α → R} (h : IsGroupLike a) : coeff a [] = 1

theorem RoughPaths.Word.IsGroupLike.shuffle {α : Type u} {R : Type w} [Semiring R] {a : List α → R} (h : IsGroupLike a) (u v : List α) : coeff a u * coeff a v = shuffleCoeff a u v

theorem RoughPaths.Word.unit_isGroupLike {α : Type u} {R : Type w} [Semiring R] : IsGroupLike (unit α R)

theorem RoughPaths.Word.IsGroupLike.comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} [Semiring R] {a : List δ → R} (h : IsGroupLike a) (f : γ → δ) : IsGroupLike (Word.comapMapLetters f a)

def RoughPaths.Word.tensorProduct {α : Type u} {R : Type w} [AddMonoid R] [Mul R] (a b : List α → R) : List α → R

Concatenation, or tensor, product of two word-indexed series.

Equations

• RoughPaths.Word.tensorProduct a b w = (List.map (fun (p : List α × List α) => RoughPaths.Word.coeff a p.1 * RoughPaths.Word.coeff b p.2) (HopfAlgebras.Word.splits w)).sum

@[simp]

theorem RoughPaths.Word.tensorProduct_nil {α : Type u} {R : Type w} [AddMonoid R] [Mul R] (a b : List α → R) : coeff (tensorProduct a b) [] = coeff a [] * coeff b []

theorem RoughPaths.Word.tensorProduct_cons {α : Type u} {R : Type w} [AddMonoid R] [Mul R] (a b : List α → R) (x : α) (w : List α) : coeff (tensorProduct a b) (x :: w) = coeff a [] * coeff b (x :: w) + (List.map (fun (p : List α × List α) => coeff a (x :: p.1) * coeff b p.2) (HopfAlgebras.Word.splits w)).sum

theorem RoughPaths.Word.tensorProduct_comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} [AddMonoid R] [Mul R] (f : γ → δ) (a b : List δ → R) : tensorProduct (comapMapLetters f a) (comapMapLetters f b) = comapMapLetters f (tensorProduct a b)

@[simp]

theorem RoughPaths.Word.tensorProduct_unit_left {α : Type u} {R : Type w} [Semiring R] (a : List α → R) : tensorProduct (unit α R) a = a

@[simp]

theorem RoughPaths.Word.tensorProduct_unit_right {α : Type u} {R : Type w} [Semiring R] (a : List α → R) : tensorProduct a (unit α R) = a

theorem RoughPaths.Word.tensorProduct_hasUnitEmpty {α : Type u} {R : Type w} [Semiring R] {a b : List α → R} (ha : HasUnitEmpty a) (hb : HasUnitEmpty b) : HasUnitEmpty (tensorProduct a b)

theorem RoughPaths.Word.tensorProduct_assoc {α : Type u} {R : Type w} [Semiring R] (a b c : List α → R) : tensorProduct (tensorProduct a b) c = tensorProduct a (tensorProduct b c)

@[reducible, inline]

abbrev RoughPaths.Word.Truncation (α : Type u) (R : Type v) (n : ℕ) : Type (max u v)

Truncation of a signature series to words of length at most n.

Equations

• RoughPaths.Word.Truncation α R n = ({ w : List α // w.length ≤ n } → R)

def RoughPaths.Word.truncate {α : Type u} {R : Type w} (a : List α → R) (n : ℕ) : Truncation α R n

Restrict a signature series to words of length at most n.

Equations

• RoughPaths.Word.truncate a n w = RoughPaths.Word.coeff a ↑w

@[simp]

theorem RoughPaths.Word.truncate_apply {α : Type u} {R : Type w} (a : List α → R) (n : ℕ) (w : { w : List α // w.length ≤ n }) : truncate a n w = coeff a ↑w

theorem RoughPaths.Word.truncate_ext {α : Type u} {R : Type w} {a b : List α → R} {n : ℕ} (h : ∀ (w : List α), w.length ≤ n → coeff a w = coeff b w) : truncate a n = truncate b n

theorem RoughPaths.Word.truncate_eq_iff_agreeUpToDegree {α : Type u} {R : Type w} (a b : List α → R) (n : ℕ) : truncate a n = truncate b n ↔ ∀ (w : List α), w.length ≤ n → coeff a w = coeff b w

theorem RoughPaths.Word.truncate_comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} (f : γ → δ) (a : List δ → R) (n : ℕ) : truncate (comapMapLetters f a) n = fun (w : { w : List γ // w.length ≤ n }) => coeff a (List.map f ↑w)

def RoughPaths.Word.AgreeUpToDegree {α : Type u} {R : Type w} (a b : List α → R) (n : ℕ) : Prop

Agreement of two signature series through word degree n.

Equations

• RoughPaths.Word.AgreeUpToDegree a b n = ∀ (w : List α), w.length ≤ n → RoughPaths.Word.coeff a w = RoughPaths.Word.coeff b w

theorem RoughPaths.Word.agreeUpToDegree_refl {α : Type u} {R : Type w} (a : List α → R) (n : ℕ) : AgreeUpToDegree a a n

theorem RoughPaths.Word.AgreeUpToDegree.symm {α : Type u} {R : Type w} {a b : List α → R} {n : ℕ} (h : AgreeUpToDegree a b n) : AgreeUpToDegree b a n

theorem RoughPaths.Word.AgreeUpToDegree.trans {α : Type u} {R : Type w} {a b c : List α → R} {n : ℕ} (hab : AgreeUpToDegree a b n) (hbc : AgreeUpToDegree b c n) : AgreeUpToDegree a c n

theorem RoughPaths.Word.AgreeUpToDegree.mono {α : Type u} {R : Type w} {a b : List α → R} {m n : ℕ} (h : AgreeUpToDegree a b n) (hmn : m ≤ n) : AgreeUpToDegree a b m

theorem RoughPaths.Word.AgreeUpToDegree.comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} {a b : List δ → R} {n : ℕ} (h : AgreeUpToDegree a b n) (f : γ → δ) : AgreeUpToDegree (Word.comapMapLetters f a) (Word.comapMapLetters f b) n

theorem RoughPaths.Word.agreeUpToDegree_succ_iff {α : Type u} {R : Type w} {a b : List α → R} {n : ℕ} : AgreeUpToDegree a b (n + 1) ↔ AgreeUpToDegree a b n ∧ ∀ (w : List α), w.length = n + 1 → coeff a w = coeff b w

theorem RoughPaths.Word.agreeUpToDegree_of_eq {α : Type u} {R : Type w} {a b : List α → R} (h : a = b) (n : ℕ) : AgreeUpToDegree a b n

theorem RoughPaths.Word.eq_of_agreeUpToDegree_all {α : Type u} {R : Type w} {a b : List α → R} (h : ∀ (n : ℕ), AgreeUpToDegree a b n) : a = b

theorem RoughPaths.Word.agreeUpToDegree_all_iff_eq {α : Type u} {R : Type w} {a b : List α → R} : (∀ (n : ℕ), AgreeUpToDegree a b n) ↔ a = b

theorem RoughPaths.Word.truncate_eq_iff {α : Type u} {R : Type w} (a b : List α → R) (n : ℕ) : truncate a n = truncate b n ↔ AgreeUpToDegree a b n

theorem RoughPaths.Word.agreeUpToDegree_tensorProduct {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a a' b b' : List α → R} {n : ℕ} (ha : AgreeUpToDegree a a' n) (hb : AgreeUpToDegree b b' n) : AgreeUpToDegree (tensorProduct a b) (tensorProduct a' b') n

theorem RoughPaths.Word.agreeUpToDegree_tensorProduct_left {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a a' b : List α → R} {n : ℕ} (ha : AgreeUpToDegree a a' n) : AgreeUpToDegree (tensorProduct a b) (tensorProduct a' b) n

theorem RoughPaths.Word.agreeUpToDegree_tensorProduct_right {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a b b' : List α → R} {n : ℕ} (hb : AgreeUpToDegree b b' n) : AgreeUpToDegree (tensorProduct a b) (tensorProduct a b') n

theorem RoughPaths.Word.tensorProduct_eq_of_agreeUpToDegree_all {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a a' b b' : List α → R} (ha : ∀ (n : ℕ), AgreeUpToDegree a a' n) (hb : ∀ (n : ℕ), AgreeUpToDegree b b' n) : tensorProduct a b = tensorProduct a' b'

theorem RoughPaths.Word.tensorProduct_left_eq_of_agreeUpToDegree_all {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a a' b : List α → R} (ha : ∀ (n : ℕ), AgreeUpToDegree a a' n) : tensorProduct a b = tensorProduct a' b

theorem RoughPaths.Word.tensorProduct_right_eq_of_agreeUpToDegree_all {α : Type u} {R : Type w} [AddMonoid R] [Mul R] {a b b' : List α → R} (hb : ∀ (n : ℕ), AgreeUpToDegree b b' n) : tensorProduct a b = tensorProduct a b'

def RoughPaths.Word.SatisfiesShuffleUpToDegree {α : Type u} {R : Type w} [Semiring R] (a : List α → R) (n : ℕ) : Prop

The shuffle identity restricted to pairs with total degree at most n.

Equations

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

theorem RoughPaths.Word.IsGroupLike.satisfiesShuffleUpToDegree {α : Type u} {R : Type w} [Semiring R] {a : List α → R} (h : IsGroupLike a) (n : ℕ) : SatisfiesShuffleUpToDegree a n

theorem RoughPaths.Word.SatisfiesShuffleUpToDegree.mono {α : Type u} {R : Type w} [Semiring R] {a : List α → R} {m n : ℕ} (h : SatisfiesShuffleUpToDegree a n) (hmn : m ≤ n) : SatisfiesShuffleUpToDegree a m

theorem RoughPaths.Word.SatisfiesShuffleUpToDegree.comapMapLetters {R : Type w} {γ : Type u} {δ : Type v} [Semiring R] {a : List δ → R} {n : ℕ} (h : SatisfiesShuffleUpToDegree a n) (f : γ → δ) : SatisfiesShuffleUpToDegree (Word.comapMapLetters f a) n

theorem RoughPaths.Word.isGroupLike_iff_satisfiesShuffleUpToDegree_all {α : Type u} {R : Type w} [Semiring R] {a : List α → R} : IsGroupLike a ↔ ∀ (n : ℕ), SatisfiesShuffleUpToDegree a n

theorem RoughPaths.Word.unit_satisfiesShuffleUpToDegree {α : Type u} {R : Type w} [Semiring R] (n : ℕ) : SatisfiesShuffleUpToDegree (unit α R) n

theorem RoughPaths.isCharacter_wordHopf_iff {α : Type u} {R : Type v} [CommSemiring R] (φ : List α → R) : (HopfAlgebras.wordHopf α).IsCharacter φ ↔ Word.IsGroupLike φ

Group-like signature series are exactly the characters of the word shuffle Hopf algebra — definitionally.

theorem RoughPaths.tensorProduct_eq_conv {α : Type u} {R : Type v} [CommSemiring R] (A B : List α → R) : Word.tensorProduct A B = HopfAlgebras.CombBialg.Character.conv A B

The tensor (Chen) product of series is the convolution product dual to deconcatenation — definitionally.

@[reducible, inline]

abbrev RoughPaths.Signature (α : Type u) (R : Type v) [CommSemiring R] : Type (max u v)

A signature: a character of the word shuffle Hopf algebra — this is the character type (wordHopf α).Character R, i.e. the subtype of group-like (shuffle-multiplicative, normalized) signature series. The monoid structure (tensor/Chen product) and, over a commutative ring, the group structure (shuffle antipode inverse) come from the abstract character theory of HopfAlgebras.Combinatorial.Basic.

Equations

• RoughPaths.Signature α R = (HopfAlgebras.wordHopf α).Character R

theorem RoughPaths.Signature.one_val {α : Type u} {R : Type v} [CommSemiring R] : ↑1 = Word.unit α R

The underlying series of the convolution unit is the unit series.

theorem RoughPaths.Signature.mul_val {α : Type u} {R : Type v} [CommSemiring R] (σ τ : Signature α R) : ↑(σ * τ) = Word.tensorProduct ↑σ ↑τ

The underlying series of a product is the tensor product.

def RoughPaths.Signature.coeff {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) (w : List α) : R

The coefficient of a word in a bundled signature.

Equations

• σ.coeff w = RoughPaths.Word.coeff (↑σ) w

@[simp]

theorem RoughPaths.Signature.coeff_apply {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) (w : List α) : σ.coeff w = ↑σ w

@[simp]

theorem RoughPaths.Signature.coeff_nil {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) : σ.coeff [] = 1

theorem RoughPaths.Signature.ext {α : Type u} {R : Type v} [CommSemiring R] {σ τ : Signature α R} (h : ∀ (w : List α), σ.coeff w = τ.coeff w) : σ = τ

theorem RoughPaths.Signature.ext_iff {α : Type u} {R : Type v} [CommSemiring R] {σ τ : Signature α R} : σ = τ ↔ ∀ (w : List α), σ.coeff w = τ.coeff w

def RoughPaths.Signature.unit (α : Type u) (R : Type v) [CommSemiring R] : Signature α R

The identity signature.

Equations

• RoughPaths.Signature.unit α R = ⟨RoughPaths.Word.unit α R, ⋯⟩

theorem RoughPaths.Signature.unit_eq_one {α : Type u} {R : Type v} [CommSemiring R] : unit α R = 1

The identity signature is the convolution unit of the character monoid.

@[simp]

theorem RoughPaths.Signature.unit_coeff_nil {α : Type u} {R : Type v} [CommSemiring R] : (unit α R).coeff [] = 1

@[simp]

theorem RoughPaths.Signature.unit_coeff_cons {α : Type u} {R : Type v} [CommSemiring R] (x : α) (w : List α) : (unit α R).coeff (x :: w) = 0

theorem RoughPaths.Signature.shuffle {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) (u v : List α) : σ.coeff u * σ.coeff v = Word.shuffleCoeff (↑σ) u v

theorem RoughPaths.Signature.satisfiesShuffleUpToDegree {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) (n : ℕ) : Word.SatisfiesShuffleUpToDegree (↑σ) n

def RoughPaths.Signature.comapMapLetters {R : Type v} [CommSemiring R] {γ : Type u} {δ : Type z} (f : γ → δ) (σ : Signature δ R) : Signature γ R

Relabel a bundled signature by mapping letters.

Equations

• RoughPaths.Signature.comapMapLetters f σ = ⟨RoughPaths.Word.comapMapLetters f ↑σ, ⋯⟩

@[simp]

theorem RoughPaths.Signature.coeff_comapMapLetters {R : Type v} [CommSemiring R] {γ : Type u} {δ : Type z} (f : γ → δ) (σ : Signature δ R) (w : List γ) : (comapMapLetters f σ).coeff w = σ.coeff (List.map f w)

@[simp]

theorem RoughPaths.Signature.comapMapLetters_id {α : Type u} {R : Type v} [CommSemiring R] (σ : Signature α R) : comapMapLetters id σ = σ

theorem RoughPaths.Signature.comapMapLetters_comp {R : Type v} [CommSemiring R] {γ : Type u} {δ : Type z} {ε : Type w} (f : γ → δ) (g : δ → ε) (σ : Signature ε R) : comapMapLetters f (comapMapLetters g σ) = comapMapLetters (g ∘ f) σ

@[simp]

theorem RoughPaths.Signature.comapMapLetters_unit {R : Type v} [CommSemiring R] {γ : Type u} {δ : Type z} (f : γ → δ) : comapMapLetters f (unit δ R) = unit γ R