Truncated Log-Signatures

This file adds tensor powers and finite tensor exponential/logarithm series for word-indexed signatures. The logarithm is defined by applying the usual finite log (1 + x) polynomial to the augmentation part of a signature. The finite tensor exponential and logarithm are natural under relabelling of the alphabet.

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

The zero word-indexed series.

Equations

• RoughPaths.Word.zero α R x✝ = 0

@[simp]

theorem RoughPaths.Word.coeff_zero {α : Type u} {R : Type v} [Zero R] (w : List α) : coeff (zero α R) w = 0

@[simp]

theorem RoughPaths.Word.tensorProduct_zero_left {α : Type u} {R : Type v} [Semiring R] (a : List α → R) : tensorProduct (zero α R) a = zero α R

@[simp]

theorem RoughPaths.Word.tensorProduct_zero_right {α : Type u} {R : Type v} [Semiring R] (a : List α → R) : tensorProduct a (zero α R) = zero α R

def RoughPaths.Word.tensorPower {α : Type u} {R : Type v} [Semiring R] (a : List α → R) : ℕ → List α → R

Tensor powers for the concatenation product.

Equations

• RoughPaths.Word.tensorPower a 0 = RoughPaths.Word.unit α R
• RoughPaths.Word.tensorPower a n.succ = RoughPaths.Word.tensorProduct a (RoughPaths.Word.tensorPower a n)

@[simp]

theorem RoughPaths.Word.tensorPower_zero {α : Type u} {R : Type v} [Semiring R] (a : List α → R) : tensorPower a 0 = unit α R

@[simp]

theorem RoughPaths.Word.tensorPower_succ {α : Type u} {R : Type v} [Semiring R] (a : List α → R) (n : ℕ) : tensorPower a (n + 1) = tensorProduct a (tensorPower a n)

@[simp]

theorem RoughPaths.Word.tensorPower_one {α : Type u} {R : Type v} [Semiring R] (a : List α → R) : tensorPower a 1 = a

theorem RoughPaths.Word.tensorPower_add {α : Type u} {R : Type v} [Semiring R] (a : List α → R) (m n : ℕ) : tensorPower a (m + n) = tensorProduct (tensorPower a m) (tensorPower a n)

theorem RoughPaths.Word.tensorPower_succ_right {α : Type u} {R : Type v} [Semiring R] (a : List α → R) (n : ℕ) : tensorPower a (n + 1) = tensorProduct (tensorPower a n) a

@[simp]

theorem RoughPaths.Word.tensorPower_unit {α : Type u} {R : Type v} [Semiring R] (n : ℕ) : tensorPower (unit α R) n = unit α R

@[simp]

theorem RoughPaths.Word.tensorPower_zero_succ {α : Type u} {R : Type v} [Semiring R] (n : ℕ) : tensorPower (zero α R) (n + 1) = zero α R

theorem RoughPaths.Word.tensorPower_coeff_nil {α : Type u} {R : Type v} [Semiring R] (a : List α → R) (n : ℕ) : coeff (tensorPower a n) [] = coeff a [] ^ n

theorem RoughPaths.Word.tensorPower_hasUnitEmpty {α : Type u} {R : Type v} [Semiring R] {a : List α → R} (ha : HasUnitEmpty a) (n : ℕ) : HasUnitEmpty (tensorPower a n)

theorem RoughPaths.Word.agreeUpToDegree_tensorPower {α : Type u} {R : Type v} [Semiring R] {a b : List α → R} {n : ℕ} (h : AgreeUpToDegree a b n) (k : ℕ) : AgreeUpToDegree (tensorPower a k) (tensorPower b k) n

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

def RoughPaths.Word.augmentationPart {α : Type u} {R : Type v} [Sub R] [Zero R] [One R] (a : List α → R) : List α → R

The augmentation part a - 1 of a series.

Equations

• RoughPaths.Word.augmentationPart a w = RoughPaths.Word.coeff a w - RoughPaths.Word.coeff (RoughPaths.Word.unit α R) w

@[simp]

theorem RoughPaths.Word.coeff_augmentationPart {α : Type u} {R : Type v} [Sub R] [Zero R] [One R] (a : List α → R) (w : List α) : coeff (augmentationPart a) w = coeff a w - coeff (unit α R) w

theorem RoughPaths.Word.coeff_augmentationPart_nil {α : Type u} {R : Type v} [Ring R] {a : List α → R} (ha : HasUnitEmpty a) : coeff (augmentationPart a) [] = 0

@[simp]

theorem RoughPaths.Word.augmentationPart_unit {α : Type u} {R : Type v} [Ring R] : augmentationPart (unit α R) = zero α R

theorem RoughPaths.Word.agreeUpToDegree_augmentationPart {α : Type u} {R : Type v} [Ring R] {a b : List α → R} {n : ℕ} (h : AgreeUpToDegree a b n) : AgreeUpToDegree (augmentationPart a) (augmentationPart b) n

theorem RoughPaths.Word.augmentationPart_comapMapLetters {R : Type v} {γ : Type u} {δ : Type w} [Ring R] (f : γ → δ) (a : List δ → R) : augmentationPart (comapMapLetters f a) = comapMapLetters f (augmentationPart a)

def RoughPaths.Word.tensorExpTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) : List α → R

Finite tensor exponential ∑_{k=0}^n a^{⊗k}/k!.

Equations

• RoughPaths.Word.tensorExpTruncated a n w = (List.map (fun (k : ℕ) => (↑k.factorial)⁻¹ * RoughPaths.Word.coeff (RoughPaths.Word.tensorPower a k) w) (List.range (n + 1))).sum

@[simp]

theorem RoughPaths.Word.coeff_tensorExpTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) (w : List α) : coeff (tensorExpTruncated a n) w = (List.map (fun (k : ℕ) => (↑k.factorial)⁻¹ * coeff (tensorPower a k) w) (List.range (n + 1))).sum

@[simp]

theorem RoughPaths.Word.tensorExpTruncated_zero {α : Type u} {R : Type v} [Field R] (a : List α → R) : tensorExpTruncated a 0 = unit α R

theorem RoughPaths.Word.agreeUpToDegree_tensorExpTruncated {α : Type u} {R : Type v} [Field R] {a b : List α → R} {m n : ℕ} (h : AgreeUpToDegree a b n) : AgreeUpToDegree (tensorExpTruncated a m) (tensorExpTruncated b m) n

theorem RoughPaths.Word.tensorExpTruncated_comapMapLetters {R : Type v} {γ : Type u} {δ : Type w} [Field R] (f : γ → δ) (a : List δ → R) (n : ℕ) : tensorExpTruncated (comapMapLetters f a) n = comapMapLetters f (tensorExpTruncated a n)

def RoughPaths.Word.tensorLogOnePlusTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) : List α → R

Finite tensor logarithm ∑_{k=1}^n (-1)^{k+1} a^{⊗k}/k.

Equations

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

@[simp]

theorem RoughPaths.Word.coeff_tensorLogOnePlusTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) (w : List α) : coeff (tensorLogOnePlusTruncated a n) w = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * coeff (tensorPower a k) w) (List.range n)).sum

@[simp]

theorem RoughPaths.Word.tensorLogOnePlusTruncated_zero {α : Type u} {R : Type v} [Field R] (a : List α → R) : tensorLogOnePlusTruncated a 0 = zero α R

@[simp]

theorem RoughPaths.Word.tensorLogOnePlusTruncated_zero_series {α : Type u} {R : Type v} [Field R] (n : ℕ) : tensorLogOnePlusTruncated (zero α R) n = zero α R

theorem RoughPaths.Word.agreeUpToDegree_tensorLogOnePlusTruncated {α : Type u} {R : Type v} [Field R] {a b : List α → R} {m n : ℕ} (h : AgreeUpToDegree a b n) : AgreeUpToDegree (tensorLogOnePlusTruncated a m) (tensorLogOnePlusTruncated b m) n

theorem RoughPaths.Word.tensorLogOnePlusTruncated_comapMapLetters {R : Type v} {γ : Type u} {δ : Type w} [Field R] (f : γ → δ) (a : List δ → R) (n : ℕ) : tensorLogOnePlusTruncated (comapMapLetters f a) n = comapMapLetters f (tensorLogOnePlusTruncated a n)

def RoughPaths.Word.logSignatureTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) : List α → R

Truncated log-signature, defined as log (1 + (a - 1)).

Equations

• RoughPaths.Word.logSignatureTruncated a n = RoughPaths.Word.tensorLogOnePlusTruncated (RoughPaths.Word.augmentationPart a) n

@[simp]

theorem RoughPaths.Word.coeff_logSignatureTruncated {α : Type u} {R : Type v} [Field R] (a : List α → R) (n : ℕ) (w : List α) : coeff (logSignatureTruncated a n) w = coeff (tensorLogOnePlusTruncated (augmentationPart a) n) w

@[simp]

theorem RoughPaths.Word.logSignatureTruncated_zero {α : Type u} {R : Type v} [Field R] (a : List α → R) : logSignatureTruncated a 0 = zero α R

@[simp]

theorem RoughPaths.Word.logSignatureTruncated_unit {α : Type u} {R : Type v} [Field R] (n : ℕ) : logSignatureTruncated (unit α R) n = zero α R

theorem RoughPaths.Word.agreeUpToDegree_logSignatureTruncated {α : Type u} {R : Type v} [Field R] {a b : List α → R} {m n : ℕ} (h : AgreeUpToDegree a b n) : AgreeUpToDegree (logSignatureTruncated a m) (logSignatureTruncated b m) n

theorem RoughPaths.Word.logSignatureTruncated_comapMapLetters {R : Type v} {γ : Type u} {δ : Type w} [Field R] (f : γ → δ) (a : List δ → R) (n : ℕ) : logSignatureTruncated (comapMapLetters f a) n = comapMapLetters f (logSignatureTruncated a n)

def RoughPaths.Signature.logTruncated {α : Type u} {R : Type v} [Field R] (σ : Signature α R) (n : ℕ) : List α → R

The truncated log-signature of a bundled signature.

Equations

• σ.logTruncated n = RoughPaths.Word.logSignatureTruncated (↑σ) n

@[simp]

theorem RoughPaths.Signature.coeff_logTruncated {α : Type u} {R : Type v} [Field R] (σ : Signature α R) (n : ℕ) (w : List α) : Word.coeff (σ.logTruncated n) w = Word.coeff (Word.logSignatureTruncated (↑σ) n) w

@[simp]

theorem RoughPaths.Signature.logTruncated_zero {α : Type u} {R : Type v} [Field R] (σ : Signature α R) : σ.logTruncated 0 = Word.zero α R

theorem RoughPaths.Signature.logTruncated_comapMapLetters {R : Type v} [Field R] {γ : Type u} {δ : Type w} (f : γ → δ) (σ : Signature δ R) (n : ℕ) : (comapMapLetters f σ).logTruncated n = Word.comapMapLetters f (σ.logTruncated n)

def RoughPaths.AlgebraicRoughPath.logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicRoughPath T α R) (s t : T) (n : ℕ) : List α → R

The truncated log-signature of an algebraic rough path increment.

Equations

• X.logIncrementTruncated s t n = RoughPaths.Word.logSignatureTruncated (X.increment s t) n

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicRoughPath T α R) (s t : T) (n : ℕ) (word : List α) : Word.coeff (X.logIncrementTruncated s t n) word = Word.coeff (Word.logSignatureTruncated (X.increment s t) n) word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.logIncrementTruncated_zero {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicRoughPath T α R) (s t : T) : X.logIncrementTruncated s t 0 = Word.zero α R

@[simp]

theorem RoughPaths.AlgebraicRoughPath.logIncrementTruncated_self {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicRoughPath T α R) (t : T) (n : ℕ) : X.logIncrementTruncated t t n = Word.zero α R

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_logIncrementTruncated_self {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicRoughPath T α R) (t : T) (n : ℕ) (word : List α) : Word.coeff (X.logIncrementTruncated t t n) word = 0

theorem RoughPaths.AlgebraicRoughPath.AgreeUpToDegree.logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] {X Y : AlgebraicRoughPath T α R} {m n : ℕ} (h : X.AgreeUpToDegree Y n) (s t : T) : Word.AgreeUpToDegree (X.logIncrementTruncated s t m) (Y.logIncrementTruncated s t m) n

theorem RoughPaths.AlgebraicRoughPath.AgreeUpToDegree.logIncrementTruncated_coeff {T : Type u} {α : Type v} {R : Type w} [Field R] {X Y : AlgebraicRoughPath T α R} {m n : ℕ} (h : X.AgreeUpToDegree Y n) (s t : T) (word : List α) (hword : word.length ≤ n) : Word.coeff (X.logIncrementTruncated s t m) word = Word.coeff (Y.logIncrementTruncated s t m) word

theorem RoughPaths.AlgebraicRoughPath.logIncrementTruncated_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) (s t : T) (n : ℕ) : (comapMapLetters f X).logIncrementTruncated s t n = Word.comapMapLetters f (X.logIncrementTruncated s t n)

theorem RoughPaths.AlgebraicRoughPath.logIncrementTruncated_comapMapLetters_coeff {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) (s t : T) (n : ℕ) (word : List α) : Word.coeff ((comapMapLetters f X).logIncrementTruncated s t n) word = Word.coeff (X.logIncrementTruncated s t n) (List.map f word)