Algebraic Rough Paths

This file defines the algebraic part of a rough path: a two-parameter family of word signatures satisfying Chen's identity. Analytic regularity, such as finite p-variation or Holder bounds, is deliberately left for later files.

Main definitions

• AlgebraicRoughPath - group-like signature increments satisfying Chen's identity
• AlgebraicRoughPath.unit - the constant identity rough path
• AlgebraicRoughPath.coeff - coordinate of an increment on a word
• AlgebraicRoughPath.chen_coeff - coefficient form of Chen's identity
• AlgebraicRoughPath.increment_tensorProduct_reverse - reverse increments multiply to the unit

References

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

structure RoughPaths.AlgebraicRoughPath (T : Type u) (α : Type v) (R : Type w) [Semiring R] : Type (max (max u v) w)

Algebraic rough path increments: a multiplicative functional on words. identity and chen are Chen's relations and unitEmpty normalises the degree-zero coefficient. Geometricity (the shuffle identity) is the separate mixin IsWeaklyGeometric, so general non-geometric (e.g. Itô-type) rough paths are included.

• increment : T → T → List α → R
• identity (t : T) : self.increment t t = Word.unit α R
• chen (s t u : T) : self.increment s u = Word.tensorProduct (self.increment s t) (self.increment t u)
• unitEmpty (s t : T) : Word.coeff (self.increment s t) [] = 1

def RoughPaths.AlgebraicRoughPath.IsWeaklyGeometric {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) : Prop

A rough path is weakly geometric when every increment is group-like, i.e. satisfies the shuffle identity.

Equations

• X.IsWeaklyGeometric = ∀ (s t : T), RoughPaths.Word.IsGroupLike (X.increment s t)

def RoughPaths.AlgebraicRoughPath.unit (T : Type u) (α : Type v) (R : Type w) [Semiring R] : AlgebraicRoughPath T α R

The constant identity word-signature rough path.

Equations

• RoughPaths.AlgebraicRoughPath.unit T α R = { increment := fun (x x_1 : T) => RoughPaths.Word.unit α R, identity := ⋯, chen := ⋯, unitEmpty := ⋯ }

theorem RoughPaths.AlgebraicRoughPath.unit_isWeaklyGeometric {T : Type u} {α : Type v} {R : Type w} [Semiring R] : (unit T α R).IsWeaklyGeometric

def RoughPaths.AlgebraicRoughPath.comapTime {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) (X : AlgebraicRoughPath T α R) : AlgebraicRoughPath S α R

Pull an algebraic rough path back along a map of time domains.

Equations

• RoughPaths.AlgebraicRoughPath.comapTime f X = { increment := fun (s t : S) => X.increment (f s) (f t), identity := ⋯, chen := ⋯, unitEmpty := ⋯ }

def RoughPaths.AlgebraicRoughPath.comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) : AlgebraicRoughPath T α R

Pull an algebraic rough path back along a map of alphabets.

Equations

• RoughPaths.AlgebraicRoughPath.comapMapLetters f X = { increment := fun (s t : T) => RoughPaths.Word.comapMapLetters f (X.increment s t), identity := ⋯, chen := ⋯, unitEmpty := ⋯ }

theorem RoughPaths.AlgebraicRoughPath.IsWeaklyGeometric.comapTime {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) {X : AlgebraicRoughPath T α R} (hX : X.IsWeaklyGeometric) : (AlgebraicRoughPath.comapTime f X).IsWeaklyGeometric

theorem RoughPaths.AlgebraicRoughPath.IsWeaklyGeometric.comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) {X : AlgebraicRoughPath T β R} (hX : X.IsWeaklyGeometric) : (AlgebraicRoughPath.comapMapLetters f X).IsWeaklyGeometric

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapMapLetters_increment {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) (s t : T) : (comapMapLetters f X).increment s t = Word.comapMapLetters f (X.increment s t)

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapTime_increment {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) (X : AlgebraicRoughPath T α R) (s t : S) : (comapTime f X).increment s t = X.increment (f s) (f t)

def RoughPaths.AlgebraicRoughPath.coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (word : List α) : R

Coordinate of an algebraic rough path increment on a word.

Equations

• X.coeff s t word = RoughPaths.Word.coeff (X.increment s t) word

def RoughPaths.AlgebraicRoughPath.truncatedIncrement {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : T) : Word.Truncation α R n

Equations

• X.truncatedIncrement n s t = RoughPaths.Word.truncate (X.increment s t) n

theorem RoughPaths.AlgebraicRoughPath.ext {T : Type u} {α : Type v} {R : Type w} [Semiring R] {X Y : AlgebraicRoughPath T α R} (h : ∀ (s t : T) (word : List α), X.coeff s t word = Y.coeff s t word) : X = Y

theorem RoughPaths.AlgebraicRoughPath.ext_iff {T : Type u} {α : Type v} {R : Type w} [Semiring R] {X Y : AlgebraicRoughPath T α R} : X = Y ↔ ∀ (s t : T) (word : List α), X.coeff s t word = Y.coeff s t word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.unit_increment {T : Type u} {α : Type v} {R : Type w} [Semiring R] (s t : T) : (unit T α R).increment s t = Word.unit α R

theorem RoughPaths.AlgebraicRoughPath.unit_coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (s t : T) (word : List α) : (unit T α R).coeff s t word = Word.coeff (Word.unit α R) word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.unit_coeff_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (s t : T) : (unit T α R).coeff s t [] = 1

@[simp]

theorem RoughPaths.AlgebraicRoughPath.unit_coeff_cons {T : Type u} {α : Type v} {R : Type w} [Semiring R] (s t : T) (x : α) (word : List α) : (unit T α R).coeff s t (x :: word) = 0

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) (s t : T) (word : List α) : (comapMapLetters f X).coeff s t word = X.coeff s t (List.map f word)

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_comapTime {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) (X : AlgebraicRoughPath T α R) (s t : S) (word : List α) : (comapTime f X).coeff s t word = X.coeff (f s) (f t) word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.truncatedIncrement_apply {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : T) (word : { word : List α // word.length ≤ n }) : X.truncatedIncrement n s t word = X.coeff s t ↑word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.truncatedIncrement_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) (X : AlgebraicRoughPath T β R) (n : ℕ) (s t : T) : (comapMapLetters f X).truncatedIncrement n s t = fun (word : { word : List α // word.length ≤ n }) => X.coeff s t (List.map f ↑word)

@[simp]

theorem RoughPaths.AlgebraicRoughPath.truncatedIncrement_comapTime {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : S) : (comapTime f X).truncatedIncrement n s t = X.truncatedIncrement n (f s) (f t)

def RoughPaths.AlgebraicRoughPath.AgreeUpToDegree {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X Y : AlgebraicRoughPath T α R) (n : ℕ) : Prop

Two algebraic rough paths agree through word degree n if all increments do.

Equations

• X.AgreeUpToDegree Y n = ∀ (s t : T), RoughPaths.Word.AgreeUpToDegree (X.increment s t) (Y.increment s t) n

theorem RoughPaths.AlgebraicRoughPath.agreeUpToDegree_refl {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (n : ℕ) : X.AgreeUpToDegree X n

theorem RoughPaths.AlgebraicRoughPath.agreeUpToDegree_iff_coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X Y : AlgebraicRoughPath T α R) (n : ℕ) : X.AgreeUpToDegree Y n ↔ ∀ (s t : T) (word : List α), word.length ≤ n → X.coeff s t word = Y.coeff s t word

theorem RoughPaths.AlgebraicRoughPath.eq_of_agreeUpToDegree_all {T : Type u} {α : Type v} {R : Type w} [Semiring R] {X Y : AlgebraicRoughPath T α R} (h : ∀ (n : ℕ), X.AgreeUpToDegree Y n) : X = Y

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapTime_id {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) : comapTime id X = X

theorem RoughPaths.AlgebraicRoughPath.comapTime_comp {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} {U : Type y} (f : S → T) (g : U → S) (X : AlgebraicRoughPath T α R) : comapTime g (comapTime f X) = comapTime (f ∘ g) X

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapTime_unit {T : Type u} {α : Type v} {R : Type w} [Semiring R] {S : Type z} (f : S → T) : comapTime f (unit T α R) = unit S α R

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapMapLetters_id {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) : comapMapLetters id X = X

theorem RoughPaths.AlgebraicRoughPath.comapMapLetters_comp {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} {γ : Type y} (f : α → β) (g : β → γ) (X : AlgebraicRoughPath T γ R) : comapMapLetters f (comapMapLetters g X) = comapMapLetters (g ∘ f) X

@[simp]

theorem RoughPaths.AlgebraicRoughPath.comapMapLetters_unit {T : Type u} {α : Type v} {R : Type w} [Semiring R] {β : Type z} (f : α → β) : comapMapLetters f (unit T β R) = unit T α R

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_apply {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (word : List α) : X.coeff s t word = X.increment s t word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.increment_self {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (t : T) : X.increment t t = Word.unit α R

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_self_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (t : T) : X.coeff t t [] = 1

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_self_cons {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (t : T) (x : α) (word : List α) : X.coeff t t (x :: word) = 0

theorem RoughPaths.AlgebraicRoughPath.increment_hasUnitEmpty {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : Word.HasUnitEmpty (X.increment s t)

@[simp]

theorem RoughPaths.AlgebraicRoughPath.coeff_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : X.coeff s t [] = 1

theorem RoughPaths.AlgebraicRoughPath.IsWeaklyGeometric.shuffle {T : Type u} {α : Type v} {R : Type w} [Semiring R] {X : AlgebraicRoughPath T α R} (hX : X.IsWeaklyGeometric) (s t : T) (u v : List α) : X.coeff s t u * X.coeff s t v = Word.shuffleCoeff (X.increment s t) u v

theorem RoughPaths.AlgebraicRoughPath.IsWeaklyGeometric.satisfiesShuffleUpToDegree {T : Type u} {α : Type v} {R : Type w} [Semiring R] {X : AlgebraicRoughPath T α R} (hX : X.IsWeaklyGeometric) (s t : T) (n : ℕ) : Word.SatisfiesShuffleUpToDegree (X.increment s t) n

theorem RoughPaths.AlgebraicRoughPath.chen_eq {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) : X.increment s u = Word.tensorProduct (X.increment s t) (X.increment t u)

theorem RoughPaths.AlgebraicRoughPath.increment_tensorProduct_reverse {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : Word.tensorProduct (X.increment s t) (X.increment t s) = Word.unit α R

theorem RoughPaths.AlgebraicRoughPath.reverse_tensorProduct_increment {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : Word.tensorProduct (X.increment t s) (X.increment s t) = Word.unit α R

theorem RoughPaths.AlgebraicRoughPath.chen_eq_left_assoc {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u v : T) : X.increment s v = Word.tensorProduct (Word.tensorProduct (X.increment s t) (X.increment t u)) (X.increment u v)

theorem RoughPaths.AlgebraicRoughPath.chen_eq_right_assoc {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u v : T) : X.increment s v = Word.tensorProduct (X.increment s t) (Word.tensorProduct (X.increment t u) (X.increment u v))

theorem RoughPaths.AlgebraicRoughPath.chen_tensorProduct_assoc_on_increments {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u v : T) : Word.tensorProduct (Word.tensorProduct (X.increment s t) (X.increment t u)) (X.increment u v) = Word.tensorProduct (X.increment s t) (Word.tensorProduct (X.increment t u) (X.increment u v))

theorem RoughPaths.AlgebraicRoughPath.chen_coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) (word : List α) : X.coeff s u word = Word.coeff (Word.tensorProduct (X.increment s t) (X.increment t u)) word

theorem RoughPaths.AlgebraicRoughPath.increment_tensorProduct_reverse_coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (word : List α) : Word.coeff (Word.tensorProduct (X.increment s t) (X.increment t s)) word = Word.coeff (Word.unit α R) word

theorem RoughPaths.AlgebraicRoughPath.reverse_tensorProduct_increment_coeff {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (word : List α) : Word.coeff (Word.tensorProduct (X.increment t s) (X.increment s t)) word = Word.coeff (Word.unit α R) word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.increment_tensorProduct_reverse_coeff_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : Word.coeff (Word.tensorProduct (X.increment s t) (X.increment t s)) [] = 1

@[simp]

theorem RoughPaths.AlgebraicRoughPath.increment_tensorProduct_reverse_coeff_cons {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (x : α) (word : List α) : Word.coeff (Word.tensorProduct (X.increment s t) (X.increment t s)) (x :: word) = 0

@[simp]

theorem RoughPaths.AlgebraicRoughPath.reverse_tensorProduct_increment_coeff_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) : Word.coeff (Word.tensorProduct (X.increment t s) (X.increment s t)) [] = 1

@[simp]

theorem RoughPaths.AlgebraicRoughPath.reverse_tensorProduct_increment_coeff_cons {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (x : α) (word : List α) : Word.coeff (Word.tensorProduct (X.increment t s) (X.increment s t)) (x :: word) = 0

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_left_assoc {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u v : T) (word : List α) : X.coeff s v word = Word.coeff (Word.tensorProduct (Word.tensorProduct (X.increment s t) (X.increment t u)) (X.increment u v)) word

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_right_assoc {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u v : T) (word : List α) : X.coeff s v word = Word.coeff (Word.tensorProduct (X.increment s t) (Word.tensorProduct (X.increment t u) (X.increment u v))) word

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_nil {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) : X.coeff s u [] = X.coeff s t [] * X.coeff t u []

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_cons {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) (x : α) (word : List α) : X.coeff s u (x :: word) = Word.coeff (X.increment s t) [] * Word.coeff (X.increment t u) (x :: word) + (List.map (fun (p : List α × List α) => Word.coeff (X.increment s t) (x :: p.1) * Word.coeff (X.increment t u) p.2) (HopfAlgebras.Word.splits word)).sum

theorem RoughPaths.AlgebraicRoughPath.chen_agreeUpToDegree {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) (n : ℕ) : Word.AgreeUpToDegree (X.increment s u) (Word.tensorProduct (X.increment s t) (X.increment t u)) n

theorem RoughPaths.AlgebraicRoughPath.chen_truncatedIncrement {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t u : T) (n : ℕ) : X.truncatedIncrement n s u = Word.truncate (Word.tensorProduct (X.increment s t) (X.increment t u)) n

@[simp]

theorem RoughPaths.AlgebraicRoughPath.truncatedIncrement_self {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (t : T) (n : ℕ) : X.truncatedIncrement n t t = Word.truncate (Word.unit α R) n

theorem RoughPaths.AlgebraicRoughPath.truncatedIncrement_tensorProduct_reverse {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (n : ℕ) : Word.truncate (Word.tensorProduct (X.increment s t) (X.increment t s)) n = Word.truncate (Word.unit α R) n

theorem RoughPaths.AlgebraicRoughPath.reverse_truncatedIncrement_tensorProduct {T : Type u} {α : Type v} {R : Type w} [Semiring R] (X : AlgebraicRoughPath T α R) (s t : T) (n : ℕ) : Word.truncate (Word.tensorProduct (X.increment t s) (X.increment s t)) n = Word.truncate (Word.unit α R) n