Log-ODE Solvers

This file adds the algebraic skeleton of log-ODE solvers for rough differential equations. The actual ODE solve is represented by an abstract time-one flow map, so the definitions do not assume an analytic existence theorem.

Main definitions

• VectorFieldFlow - an abstract time-one flow for vector fields
• OneStepMap.solveAlong - composition of one-step updates along a mesh
• IteratedVectorFields.logODEStep - geometric log-ODE step

References

• Terry Lyons, Michael Caruana, Thierry Levy, Differential Equations Driven by Rough Paths
• Peter Friz, Nicolas Victoir, Multidimensional Stochastic Processes as Rough Paths
• Castell, Gaines, An efficient approximation method for stochastic differential equations by means of the exponential Lie series

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

structure RoughPaths.VectorFieldFlow (E : Type u) [Zero E] : Type u

An abstract time-one flow map for vector fields.

• timeOne : (E → E) → E → E
• timeOne_zero (y : E) : self.timeOne (fun (x : E) => 0) y = y

def RoughPaths.VectorFieldFlow.step {E : Type u} [Zero E] (Φ : VectorFieldFlow E) (F : E → E) (y : E) : E

Apply the time-one flow of a vector field.

Equations

• Φ.step F y = Φ.timeOne F y

@[simp]

theorem RoughPaths.VectorFieldFlow.step_zero {E : Type u} [Zero E] (Φ : VectorFieldFlow E) (y : E) : Φ.step (fun (x : E) => 0) y = y

@[reducible, inline]

abbrev RoughPaths.OneStepMap (T : Type u) (E : Type v) : Type (max u v)

A one-step method on a time domain T and state space E.

Equations

• RoughPaths.OneStepMap T E = (T → T → E → E)

def RoughPaths.OneStepMap.solveAlong {T : Type u} {E : Type v} (step : OneStepMap T E) : List T → E → E

Compose one-step updates along consecutive points of a mesh.

Equations

• step.solveAlong [] x✝ = x✝
• step.solveAlong [head] x✝ = x✝
• step.solveAlong (s :: t :: mesh) x✝ = step.solveAlong (t :: mesh) (step s t x✝)

@[simp]

theorem RoughPaths.OneStepMap.solveAlong_nil {T : Type u} {E : Type v} (step : OneStepMap T E) (y : E) : step.solveAlong [] y = y

@[simp]

theorem RoughPaths.OneStepMap.solveAlong_singleton {T : Type u} {E : Type v} (step : OneStepMap T E) (t : T) (y : E) : step.solveAlong [t] y = y

@[simp]

theorem RoughPaths.OneStepMap.solveAlong_cons_cons {T : Type u} {E : Type v} (step : OneStepMap T E) (s t : T) (mesh : List T) (y : E) : step.solveAlong (s :: t :: mesh) y = step.solveAlong (t :: mesh) (step s t y)

theorem RoughPaths.OneStepMap.solveAlong_congr {T : Type u} {E : Type v} {step step' : OneStepMap T E} (h : ∀ (s t : T) (y : E), step s t y = step' s t y) (mesh : List T) (y : E) : step.solveAlong mesh y = step'.solveAlong mesh y

@[simp]

theorem RoughPaths.OneStepMap.solveAlong_id {T : Type u} {E : Type v} (mesh : List T) (y : E) : solveAlong (fun (x x_1 : T) (y : E) => y) mesh y = y

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

One geometric log-ODE step over a rough path increment.

Equations

• RoughPaths.IteratedVectorFields.logODEStep Φ V X n s t y = Φ.step (V.logODEVectorField X n s t) y

@[simp]

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

@[simp]

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

@[simp]

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

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

noncomputable def RoughPaths.IteratedVectorFields.logODESolver {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : IteratedVectorFields α E) (X : AlgebraicRoughPath T α R) (n : ℕ) (mesh : List T) (y : E) : E

The geometric log-ODE solver along a time mesh.

Equations

• RoughPaths.IteratedVectorFields.logODESolver Φ V X n mesh y = RoughPaths.OneStepMap.solveAlong (fun (s t : T) (y : E) => RoughPaths.IteratedVectorFields.logODEStep Φ V X n s t y) mesh y

theorem RoughPaths.IteratedVectorFields.logODESolver_eq_of_agreeUpToDegree {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Fintype α] [DecidableEq α] [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : IteratedVectorFields α E) {X Y : AlgebraicRoughPath T α R} {n : ℕ} (h : X.AgreeUpToDegree Y n) (mesh : List T) (y : E) : logODESolver Φ V X n mesh y = logODESolver Φ V Y n mesh y