One-step solvers for branched RDEs

Log-ODE steps along branched (labelled) rough paths, extending the geometric solvers of RoughPaths.Solver.

noncomputable def RoughPaths.BranchedIteratedVectorFields.logODEStepOn {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (n : ℕ) (terms : List HopfAlgebras.RootedForest) (s t : T) (y : E) : E

One branched log-ODE step over a finite forest support.

Equations

• RoughPaths.BranchedIteratedVectorFields.logODEStepOn Φ V X n terms s t y = Φ.step (V.logODEVectorFieldOn X n terms s t) y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.logODEStepOn_self {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (n : ℕ) (terms : List HopfAlgebras.RootedForest) (t : T) (y : E) : logODEStepOn Φ V X n terms t t y = y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.logODEStepOn_zero {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (terms : List HopfAlgebras.RootedForest) (s t : T) (y : E) : logODEStepOn Φ V X 0 terms s t y = y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.logODEStepOn_comapTime {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] {S : Type z} (f : S → T) (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (n : ℕ) (terms : List HopfAlgebras.RootedForest) (s t : S) (y : E) : logODEStepOn Φ V (AlgebraicBranchedRoughPath.comapTime f X) n terms s t y = logODEStepOn Φ V X n terms (f s) (f t) y

theorem RoughPaths.BranchedIteratedVectorFields.logODEStepOn_eq_of_agreeUpToOrder {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) {X Y : AlgebraicBranchedRoughPath T R} {terms : List HopfAlgebras.RootedForest} {n : ℕ} (h : X.AgreeUpToOrder Y n) (hterms : ∀ φ ∈ terms, φ.order ≤ n) (s t : T) (y : E) : logODEStepOn Φ V X n terms s t y = logODEStepOn Φ V Y n terms s t y

noncomputable def RoughPaths.BranchedIteratedVectorFields.logODESolverOn {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (n : ℕ) (terms : List HopfAlgebras.RootedForest) (mesh : List T) (y : E) : E

The branched log-ODE solver along a time mesh.

Equations

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

theorem RoughPaths.BranchedIteratedVectorFields.logODESolverOn_eq_of_agreeUpToOrder {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : BranchedIteratedVectorFields E) {X Y : AlgebraicBranchedRoughPath T R} {terms : List HopfAlgebras.RootedForest} {n : ℕ} (h : X.AgreeUpToOrder Y n) (hterms : ∀ φ ∈ terms, φ.order ≤ n) (mesh : List T) (y : E) : logODESolverOn Φ V X n terms mesh y = logODESolverOn Φ V Y n terms mesh y

noncomputable def RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) (terms : List (HopfAlgebras.LRootedForest α)) (s t : T) (y : E) : E

One labelled branched log-ODE step over a finite labelled forest support.

Equations

• RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn Φ V X n terms s t y = Φ.step (V.logODEVectorFieldOn X n terms s t) y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn_self {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) (terms : List (HopfAlgebras.LRootedForest α)) (t : T) (y : E) : logODEStepOn Φ V X n terms t t y = y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn_zero {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (terms : List (HopfAlgebras.LRootedForest α)) (s t : T) (y : E) : logODEStepOn Φ V X 0 terms s t y = y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn_comapTime {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] {S : Type y} (f : S → T) (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) (terms : List (HopfAlgebras.LRootedForest α)) (s t : S) (y : E) : logODEStepOn Φ V (AlgebraicLabelledBranchedRoughPath.comapTime f X) n terms s t y = logODEStepOn Φ V X n terms (f s) (f t) y

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEStepOn_eq_of_agreeUpToOrder {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) {X Y : AlgebraicLabelledBranchedRoughPath T α R} {terms : List (HopfAlgebras.LRootedForest α)} {n : ℕ} (h : X.AgreeUpToOrder Y n) (hterms : ∀ φ ∈ terms, φ.order ≤ n) (s t : T) (y : E) : logODEStepOn Φ V X n terms s t y = logODEStepOn Φ V Y n terms s t y

noncomputable def RoughPaths.LabelledBranchedIteratedVectorFields.logODESolverOn {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) (terms : List (HopfAlgebras.LRootedForest α)) (mesh : List T) (y : E) : E

The labelled branched log-ODE solver along a time mesh.

Equations

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

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODESolverOn_eq_of_agreeUpToOrder {α : Type u} {R : Type v} {E : Type w} {T : Type z} [Field R] [AddCommMonoid E] [Module R E] (Φ : VectorFieldFlow E) (V : LabelledBranchedIteratedVectorFields α E) {X Y : AlgebraicLabelledBranchedRoughPath T α R} {terms : List (HopfAlgebras.LRootedForest α)} {n : ℕ} (h : X.AgreeUpToOrder Y n) (hterms : ∀ φ ∈ terms, φ.order ≤ n) (mesh : List T) (y : E) : logODESolverOn Φ V X n terms mesh y = logODESolverOn Φ V Y n terms mesh y