Branched rough differential equations

Taylor increments and log-ODE vector fields driven by branched (labelled) rough paths, indexed by rooted forests.

Branched expansions

structure RoughPaths.BranchedIteratedVectorFields (E : Type u) : Type u

Abstract elementary differentials indexed by unlabelled forests.

• eval : HopfAlgebras.RootedForest → E → E
• eval_empty (y : E) : self.eval HopfAlgebras.RootedForest.empty y = y

theorem RoughPaths.BranchedIteratedVectorFields.ext {E : Type v} {V W : BranchedIteratedVectorFields E} (h : ∀ (φ : HopfAlgebras.RootedForest) (y : E), V.eval φ y = W.eval φ y) : V = W

theorem RoughPaths.BranchedIteratedVectorFields.ext_iff {E : Type v} {V W : BranchedIteratedVectorFields E} : V = W ↔ ∀ (φ : HopfAlgebras.RootedForest) (y : E), V.eval φ y = W.eval φ y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.eval_empty_apply {E : Type v} (V : BranchedIteratedVectorFields E) (y : E) : V.eval HopfAlgebras.RootedForest.empty y = y

noncomputable def RoughPaths.BranchedIteratedVectorFields.applyCharacterOn {R : Type u} {E : Type v} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) (χ : BranchedSignature R) (terms : List HopfAlgebras.RootedForest) (y : E) : E

Apply a branched signature over a finite list of forests.

Equations

• V.applyCharacterOn χ terms y = (List.map (fun (φ : HopfAlgebras.RootedForest) => HopfAlgebras.ForestAlgebra.Character.evalForest χ φ • V.eval φ y) terms).sum

noncomputable def RoughPaths.BranchedIteratedVectorFields.applyFunctionalOn {R : Type u} {E : Type v} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) (ℓ : HopfAlgebras.ForestAlgebra.LinearFunctional R) (terms : List HopfAlgebras.RootedForest) (y : E) : E

Apply a branched infinitesimal character over a finite list of forests.

Equations

• V.applyFunctionalOn ℓ terms y = (List.map (fun (φ : HopfAlgebras.RootedForest) => ℓ.evalForest φ • V.eval φ y) terms).sum

theorem RoughPaths.BranchedIteratedVectorFields.applyCharacterOn_congr {R : Type u} {E : Type v} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) {χ ψ : BranchedSignature R} {terms : List HopfAlgebras.RootedForest} (h : ∀ φ ∈ terms, HopfAlgebras.ForestAlgebra.Character.evalForest χ φ = HopfAlgebras.ForestAlgebra.Character.evalForest ψ φ) (y : E) : V.applyCharacterOn χ terms y = V.applyCharacterOn ψ terms y

theorem RoughPaths.BranchedIteratedVectorFields.applyFunctionalOn_congr {R : Type u} {E : Type v} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) {ℓ m : HopfAlgebras.ForestAlgebra.LinearFunctional R} {terms : List HopfAlgebras.RootedForest} (h : ∀ φ ∈ terms, ℓ.evalForest φ = m.evalForest φ) (y : E) : V.applyFunctionalOn ℓ terms y = V.applyFunctionalOn m terms y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.applyFunctionalOn_zero {R : Type u} {E : Type v} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) (terms : List HopfAlgebras.RootedForest) (y : E) : V.applyFunctionalOn 0 terms y = 0

noncomputable def RoughPaths.BranchedIteratedVectorFields.taylorIncrementOn {R : Type u} {E : Type v} {T : Type w} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (terms : List HopfAlgebras.RootedForest) (s t : T) (y : E) : E

The finite branched Taylor increment driven by a branched rough path.

Equations

• V.taylorIncrementOn X terms s t y = V.applyCharacterOn (X.character s t) terms y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.taylorIncrementOn_comapTime {R : Type u} {E : Type v} {T : Type w} [CommSemiring R] [AddCommMonoid E] [Module R E] {S : Type z} (f : S → T) (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (terms : List HopfAlgebras.RootedForest) (s t : S) (y : E) : V.taylorIncrementOn (AlgebraicBranchedRoughPath.comapTime f X) terms s t y = V.taylorIncrementOn X terms (f s) (f t) y

theorem RoughPaths.BranchedIteratedVectorFields.taylorIncrementOn_eq_of_agreeUpToOrder {R : Type u} {E : Type v} {T : Type w} [CommSemiring R] [AddCommMonoid E] [Module R 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) : V.taylorIncrementOn X terms s t y = V.taylorIncrementOn Y terms s t y

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

The finite branched log-ODE vector field over a list of forests.

Equations

• V.logODEVectorFieldOn X n terms s t y = V.applyFunctionalOn (X.logIncrementTruncated s t n) terms y

@[simp]

theorem RoughPaths.BranchedIteratedVectorFields.logODEVectorFieldOn_apply {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R E] (V : BranchedIteratedVectorFields E) (X : AlgebraicBranchedRoughPath T R) (n : ℕ) (terms : List HopfAlgebras.RootedForest) (s t : T) (y : E) : V.logODEVectorFieldOn X n terms s t y = V.applyFunctionalOn (X.logIncrementTruncated s t n) terms y

@[simp]

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

@[simp]

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

@[simp]

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

theorem RoughPaths.BranchedIteratedVectorFields.logODEVectorFieldOn_eq_of_agreeUpToOrder {R : Type u} {E : Type v} {T : Type w} [Field R] [AddCommMonoid E] [Module R 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) : V.logODEVectorFieldOn X n terms s t y = V.logODEVectorFieldOn Y n terms s t y

Labelled branched expansions

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

Abstract elementary differentials indexed by labelled forests.

• eval : HopfAlgebras.LRootedForest α → E → E
• eval_empty (y : E) : self.eval HopfAlgebras.LRootedForest.empty y = y

theorem RoughPaths.LabelledBranchedIteratedVectorFields.ext {α : Type u} {E : Type z} {V W : LabelledBranchedIteratedVectorFields α E} (h : ∀ (φ : HopfAlgebras.LRootedForest α) (y : E), V.eval φ y = W.eval φ y) : V = W

theorem RoughPaths.LabelledBranchedIteratedVectorFields.ext_iff {α : Type u} {E : Type z} {V W : LabelledBranchedIteratedVectorFields α E} : V = W ↔ ∀ (φ : HopfAlgebras.LRootedForest α) (y : E), V.eval φ y = W.eval φ y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.eval_empty_apply {α : Type u} {E : Type z} (V : LabelledBranchedIteratedVectorFields α E) (y : E) : V.eval HopfAlgebras.LRootedForest.empty y = y

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

Pull labelled elementary differentials back along a relabelling map.

Equations

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

def RoughPaths.LabelledBranchedIteratedVectorFields.comapEraseLabels {α : Type u} {E : Type z} (V : BranchedIteratedVectorFields E) : LabelledBranchedIteratedVectorFields α E

Pull unlabelled elementary differentials back to labelled forests.

Equations

• RoughPaths.LabelledBranchedIteratedVectorFields.comapEraseLabels V = { eval := fun (φ : HopfAlgebras.LRootedForest α) (y : E) => V.eval φ.erase y, eval_empty := ⋯ }

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.comapMapLabels_eval {α : Type u} {β : Type v} {E : Type z} (f : α → β) (V : LabelledBranchedIteratedVectorFields β E) (φ : HopfAlgebras.LRootedForest α) (y : E) : (comapMapLabels f V).eval φ y = V.eval (HopfAlgebras.LRootedForest.mapLabels f φ) y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.comapEraseLabels_eval {α : Type u} {E : Type z} (V : BranchedIteratedVectorFields E) (φ : HopfAlgebras.LRootedForest α) (y : E) : (comapEraseLabels V).eval φ y = V.eval φ.erase y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.comapMapLabels_id {α : Type u} {E : Type z} (V : LabelledBranchedIteratedVectorFields α E) : comapMapLabels id V = V

theorem RoughPaths.LabelledBranchedIteratedVectorFields.comapMapLabels_comp {α : Type u} {β : Type v} {E : Type z} {γ : Type u} (f : α → β) (g : β → γ) (V : LabelledBranchedIteratedVectorFields γ E) : comapMapLabels f (comapMapLabels g V) = comapMapLabels (g ∘ f) V

noncomputable def RoughPaths.LabelledBranchedIteratedVectorFields.applyCharacterOn {α : Type u} {R : Type w} {E : Type z} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) (χ : LabelledBranchedSignature α R) (terms : List (HopfAlgebras.LRootedForest α)) (y : E) : E

Apply a labelled branched signature over a finite list of labelled forests.

Equations

• V.applyCharacterOn χ terms y = (List.map (fun (φ : HopfAlgebras.LRootedForest α) => HopfAlgebras.LForestAlgebra.Character.evalForest χ φ • V.eval φ y) terms).sum

noncomputable def RoughPaths.LabelledBranchedIteratedVectorFields.applyFunctionalOn {α : Type u} {R : Type w} {E : Type z} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) (ℓ : HopfAlgebras.LForestAlgebra.LinearFunctional α R) (terms : List (HopfAlgebras.LRootedForest α)) (y : E) : E

Apply a labelled branched infinitesimal character over a finite list of forests.

Equations

• V.applyFunctionalOn ℓ terms y = (List.map (fun (φ : HopfAlgebras.LRootedForest α) => ℓ.evalForest φ • V.eval φ y) terms).sum

theorem RoughPaths.LabelledBranchedIteratedVectorFields.applyCharacterOn_congr {α : Type u} {R : Type w} {E : Type z} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) {χ ψ : LabelledBranchedSignature α R} {terms : List (HopfAlgebras.LRootedForest α)} (h : ∀ φ ∈ terms, HopfAlgebras.LForestAlgebra.Character.evalForest χ φ = HopfAlgebras.LForestAlgebra.Character.evalForest ψ φ) (y : E) : V.applyCharacterOn χ terms y = V.applyCharacterOn ψ terms y

theorem RoughPaths.LabelledBranchedIteratedVectorFields.applyFunctionalOn_congr {α : Type u} {R : Type w} {E : Type z} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) {ℓ m : HopfAlgebras.LForestAlgebra.LinearFunctional α R} {terms : List (HopfAlgebras.LRootedForest α)} (h : ∀ φ ∈ terms, ℓ.evalForest φ = m.evalForest φ) (y : E) : V.applyFunctionalOn ℓ terms y = V.applyFunctionalOn m terms y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.applyFunctionalOn_zero {α : Type u} {R : Type w} {E : Type z} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) (terms : List (HopfAlgebras.LRootedForest α)) (y : E) : V.applyFunctionalOn 0 terms y = 0

noncomputable def RoughPaths.LabelledBranchedIteratedVectorFields.taylorIncrementOn {α : Type u} {R : Type w} {E : Type z} {T : Type y} [CommSemiring R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (terms : List (HopfAlgebras.LRootedForest α)) (s t : T) (y : E) : E

The finite labelled branched Taylor increment driven by a branched rough path.

Equations

• V.taylorIncrementOn X terms s t y = V.applyCharacterOn (X.lcharacter s t) terms y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.taylorIncrementOn_comapTime {α : Type u} {R : Type w} {E : Type z} {T : Type y} [CommSemiring R] [AddCommMonoid E] [Module R E] {S : Type x} (f : S → T) (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (terms : List (HopfAlgebras.LRootedForest α)) (s t : S) (y : E) : V.taylorIncrementOn (AlgebraicLabelledBranchedRoughPath.comapTime f X) terms s t y = V.taylorIncrementOn X terms (f s) (f t) y

theorem RoughPaths.LabelledBranchedIteratedVectorFields.taylorIncrementOn_eq_of_agreeUpToOrder {α : Type u} {R : Type w} {E : Type z} {T : Type y} [CommSemiring R] [AddCommMonoid E] [Module R 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) : V.taylorIncrementOn X terms s t y = V.taylorIncrementOn Y terms s t y

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

The finite labelled branched log-ODE vector field over a list of forests.

Equations

• V.logODEVectorFieldOn X n terms s t y = V.applyFunctionalOn (X.logIncrementTruncated s t n) terms y

@[simp]

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEVectorFieldOn_apply {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Field R] [AddCommMonoid E] [Module R E] (V : LabelledBranchedIteratedVectorFields α E) (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) (terms : List (HopfAlgebras.LRootedForest α)) (s t : T) (y : E) : V.logODEVectorFieldOn X n terms s t y = V.applyFunctionalOn (X.logIncrementTruncated s t n) terms y

@[simp]

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

@[simp]

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

@[simp]

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

theorem RoughPaths.LabelledBranchedIteratedVectorFields.logODEVectorFieldOn_eq_of_agreeUpToOrder {α : Type u} {R : Type w} {E : Type z} {T : Type y} [Field R] [AddCommMonoid E] [Module R 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) : V.logODEVectorFieldOn X n terms s t y = V.logODEVectorFieldOn Y n terms s t y