Rough Differential Equation Expansions

This file records the algebraic part of rough differential equation expansions. The iterated vector fields are kept abstract, so the API applies to ordinary Taylor expansions, RDE Taylor expansions, and log-ODE vector fields.

Main definitions

• Word.wordsOfLength - all words of a fixed length over a finite alphabet
• Word.wordsUpToLength - all words up to a fixed length
• IteratedVectorFields - abstract iterated vector fields indexed by words
• IteratedVectorFields.applySeriesTruncated - finite series action
• IteratedVectorFields.taylorIncrement - truncated RDE Taylor increment
• IteratedVectorFields.logODEVectorField - log-signature-driven vector field

References

• Terry Lyons, Michael Caruana, Thierry Levy, Differential Equations Driven by Rough Paths
• Peter Friz, Nicolas Victoir, Multidimensional Stochastic Processes as Rough Paths
• Martin Hairer, Kelly, Geometric versus non-geometric rough paths

Branched (forest-indexed) analogues live downstream in LeanBSeries.

def RoughPaths.Word.wordsOfLengthList (α : Type u) [Fintype α] : ℕ → List (List α)

List form of all words of a fixed length over a finite alphabet.

Equations

• RoughPaths.Word.wordsOfLengthList α 0 = [[]]
• RoughPaths.Word.wordsOfLengthList α n.succ = List.flatMap (fun (a : α) => List.map (fun (word : List α) => a :: word) (RoughPaths.Word.wordsOfLengthList α n)) Finset.univ.toList

theorem RoughPaths.Word.mem_wordsOfLengthList_iff {α : Type u} [Fintype α] {word : List α} {n : ℕ} : word ∈ wordsOfLengthList α n ↔ word.length = n

noncomputable def RoughPaths.Word.wordsOfLength (α : Type u) [Fintype α] [DecidableEq α] : ℕ → Finset (List α)

All words of a fixed length over a finite alphabet.

Equations

• RoughPaths.Word.wordsOfLength α n = (RoughPaths.Word.wordsOfLengthList α n).toFinset

@[simp]

theorem RoughPaths.Word.mem_wordsOfLength_iff {α : Type u} [Fintype α] [DecidableEq α] {word : List α} {n : ℕ} : word ∈ wordsOfLength α n ↔ word.length = n

noncomputable def RoughPaths.Word.wordsUpToLength (α : Type u) [Fintype α] [DecidableEq α] (n : ℕ) : Finset (List α)

All words whose length is at most n.

Equations

• RoughPaths.Word.wordsUpToLength α n = (Finset.range (n + 1)).biUnion fun (k : ℕ) => RoughPaths.Word.wordsOfLength α k

@[simp]

theorem RoughPaths.Word.mem_wordsUpToLength_iff {α : Type u} [Fintype α] [DecidableEq α] {word : List α} {n : ℕ} : word ∈ wordsUpToLength α n ↔ word.length ≤ n

@[simp]

theorem RoughPaths.Word.wordsUpToLength_zero {α : Type u} [Fintype α] [DecidableEq α] : wordsUpToLength α 0 = {[]}

structure RoughPaths.IteratedVectorFields (α : Type u) (E : Type v) : Type (max u v)

Abstract iterated vector fields indexed by words.

• eval : List α → E → E
• eval_empty (y : E) : self.eval [] y = y

theorem RoughPaths.IteratedVectorFields.ext {α : Type u} {E : Type z} {V W : IteratedVectorFields α E} (h : ∀ (word : List α) (y : E), V.eval word y = W.eval word y) : V = W

theorem RoughPaths.IteratedVectorFields.ext_iff {α : Type u} {E : Type z} {V W : IteratedVectorFields α E} : V = W ↔ ∀ (word : List α) (y : E), V.eval word y = W.eval word y

@[simp]

theorem RoughPaths.IteratedVectorFields.eval_empty_apply {α : Type u} {E : Type z} (V : IteratedVectorFields α E) (y : E) : V.eval [] y = y

def RoughPaths.IteratedVectorFields.comapMapLetters {α : Type u} {β : Type v} {E : Type z} (f : α → β) (V : IteratedVectorFields β E) : IteratedVectorFields α E

Pull iterated vector fields back along a map of alphabets.

Equations

• RoughPaths.IteratedVectorFields.comapMapLetters f V = { eval := fun (word : List α) (y : E) => V.eval (List.map f word) y, eval_empty := ⋯ }

@[simp]

theorem RoughPaths.IteratedVectorFields.comapMapLetters_eval {α : Type u} {β : Type v} {E : Type z} (f : α → β) (V : IteratedVectorFields β E) (word : List α) (y : E) : (comapMapLetters f V).eval word y = V.eval (List.map f word) y

@[simp]

theorem RoughPaths.IteratedVectorFields.comapMapLetters_id {α : Type u} {E : Type z} (V : IteratedVectorFields α E) : comapMapLetters id V = V

theorem RoughPaths.IteratedVectorFields.comapMapLetters_comp {α : Type u} {β : Type v} {E : Type z} {γ : Type u} (f : α → β) (g : β → γ) (V : IteratedVectorFields γ E) : comapMapLetters f (comapMapLetters g V) = comapMapLetters (g ∘ f) V

noncomputable def RoughPaths.IteratedVectorFields.applySeriesTruncated {α : Type u} {R : Type w} {E : Type z} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (a : List α → R) (n : ℕ) (y : E) : E

Apply a word-indexed series through degree n to iterated vector fields.

Equations

• V.applySeriesTruncated a n y = ∑ word ∈ RoughPaths.Word.wordsUpToLength α n, RoughPaths.Word.coeff a word • V.eval word y

theorem RoughPaths.IteratedVectorFields.applySeriesTruncated_congr {α : Type u} {R : Type w} {E : Type z} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) {a b : List α → R} {n : ℕ} (h : Word.AgreeUpToDegree a b n) (y : E) : V.applySeriesTruncated a n y = V.applySeriesTruncated b n y

@[simp]

theorem RoughPaths.IteratedVectorFields.applySeriesTruncated_zero_series {α : Type u} {R : Type w} {E : Type z} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (n : ℕ) (y : E) : V.applySeriesTruncated (Word.zero α R) n y = 0

@[simp]

theorem RoughPaths.IteratedVectorFields.applySeriesTruncated_unit {α : Type u} {R : Type w} {E : Type z} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (n : ℕ) (y : E) : V.applySeriesTruncated (Word.unit α R) n y = y

noncomputable def RoughPaths.IteratedVectorFields.taylorIncrement {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : T) (y : E) : E

The truncated Taylor increment driven by a rough path signature.

Equations

• V.taylorIncrement X n s t y = V.applySeriesTruncated (X.increment s t) n y

@[simp]

theorem RoughPaths.IteratedVectorFields.taylorIncrement_self {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (t : T) (y : E) : V.taylorIncrement X n t t y = y

@[simp]

theorem RoughPaths.IteratedVectorFields.taylorIncrement_unit {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (n : ℕ) (s t : T) (y : E) : V.taylorIncrement (AlgebraicRoughPath.unit T α R) n s t y = y

@[simp]

theorem RoughPaths.IteratedVectorFields.taylorIncrement_comapTime {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] {S : Type x} (f : S → T) (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : S) (y : E) : V.taylorIncrement (AlgebraicRoughPath.comapTime f X) n s t y = V.taylorIncrement X n (f s) (f t) y

theorem RoughPaths.IteratedVectorFields.taylorIncrement_eq_of_agreeUpToDegree {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Semiring R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) {X Y : AlgebraicRoughPath T α R} {n : ℕ} (h : X.AgreeUpToDegree Y n) (s t : T) (y : E) : V.taylorIncrement X n s t y = V.taylorIncrement Y n s t y

noncomputable def RoughPaths.IteratedVectorFields.logODEVectorField {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : T) : E → E

The log-signature vector field used by the log-ODE method.

Equations

• V.logODEVectorField X n s t y = V.applySeriesTruncated (X.logIncrementTruncated s t n) n y

@[simp]

theorem RoughPaths.IteratedVectorFields.logODEVectorField_apply {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : T) (y : E) : V.logODEVectorField X n s t y = V.applySeriesTruncated (X.logIncrementTruncated s t n) n y

@[simp]

theorem RoughPaths.IteratedVectorFields.logODEVectorField_self {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (t : T) (y : E) : V.logODEVectorField X n t t y = 0

@[simp]

theorem RoughPaths.IteratedVectorFields.logODEVectorField_zero {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (s t : T) (y : E) : V.logODEVectorField X 0 s t y = 0

@[simp]

theorem RoughPaths.IteratedVectorFields.logODEVectorField_comapTime {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] {S : Type x} (f : S → T) (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (s t : S) (y : E) : V.logODEVectorField (AlgebraicRoughPath.comapTime f X) n s t y = V.logODEVectorField X n (f s) (f t) y

theorem RoughPaths.IteratedVectorFields.logODEVectorField_eq_of_agreeUpToDegree {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (V : IteratedVectorFields α E) {X Y : AlgebraicRoughPath T α R} {n : ℕ} (h : X.AgreeUpToDegree Y n) (s t : T) (y : E) : V.logODEVectorField X n s t y = V.logODEVectorField Y n s t y