Algebraic Branched Rough Paths

This file defines the algebraic part of branched rough paths using the rooted-forest Hopf algebra already formalised in the library. Increments are characters on the forest algebra and Chen's identity is character convolution.

Analytic regularity conditions, such as finite p-variation, are not included here.

Main definitions

• AlgebraicBranchedRoughPath - unlabelled branched signature increments
• AlgebraicLabelledBranchedRoughPath - labelled branched signature increments
• AlgebraicBranchedRoughPath.increment_convolution_reverse - reverse increments convolve to the unit

References

• Massimiliano Gubinelli, Ramification of rough paths
• Christian Brouder, Alessandra Frabetti, Christian Krattenthaler, Non-commutative Hopf algebra of formal diffeomorphisms
• Peter Friz, Nicolas Victoir, Multidimensional Stochastic Processes as Rough Paths

@[reducible, inline]

abbrev RoughPaths.AlgebraicBranchedRoughPath (T : Type u) (R : Type v) [CommSemiring R] : Type (max u v)

A branched rough path is a Hopf rough path over the Butcher–Connes–Kreimer bialgebra: increments are characters on rooted forests and Chen's identity is convolution in the character monoid.

Equations

• RoughPaths.AlgebraicBranchedRoughPath T R = RoughPaths.HopfRoughPath HopfAlgebras.bckBialg T R

@[reducible, inline]

noncomputable abbrev RoughPaths.AlgebraicBranchedRoughPath.unit (T : Type u) (R : Type v) [CommSemiring R] : AlgebraicBranchedRoughPath T R

The constant identity branched rough path.

Equations

• RoughPaths.AlgebraicBranchedRoughPath.unit T R = RoughPaths.HopfRoughPath.unit HopfAlgebras.bckBialg T R

@[reducible, inline]

noncomputable abbrev RoughPaths.AlgebraicBranchedRoughPath.comapTime {T : Type u} {R : Type v} [CommSemiring R] {S : Type w} (f : S → T) (X : AlgebraicBranchedRoughPath T R) : AlgebraicBranchedRoughPath S R

Pull a branched rough path back along a map of time domains.

Equations

• RoughPaths.AlgebraicBranchedRoughPath.comapTime f X = RoughPaths.HopfRoughPath.comapTime f X

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.treeCoeff {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (τ : HopfAlgebras.RootedTree) : R

Coordinate of an increment on a rooted tree.

Equations

• X.treeCoeff s t τ = RoughPaths.HopfRoughPath.coeff X s t (HopfAlgebras.RootedForest.singleton τ)

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.character {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : HopfAlgebras.ForestAlgebra.Character R

The increment as an algebra character of the forest algebra, via the AddMonoidAlgebra.lift bridge bckCharacter.

Equations

• X.character s t = HopfAlgebras.bckCharacter ↑(X.increment s t) ⋯

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.character_evalForest {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (φ : HopfAlgebras.RootedForest) : (X.character s t).evalForest φ = HopfRoughPath.coeff X s t φ

theorem RoughPaths.AlgebraicBranchedRoughPath.ext {T : Type u} {R : Type v} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} (h : ∀ (s t : T) (φ : HopfAlgebras.RootedForest), HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ) : X = Y

theorem RoughPaths.AlgebraicBranchedRoughPath.ext_iff {T : Type u} {R : Type v} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} : X = Y ↔ ∀ (s t : T) (φ : HopfAlgebras.RootedForest), HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.coeff_comapTime {T : Type u} {R : Type v} [CommSemiring R] {S : Type w} (f : S → T) (X : AlgebraicBranchedRoughPath T R) (s t : S) (φ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff (comapTime f X) s t φ = HopfRoughPath.coeff X (f s) (f t) φ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.treeCoeff_comapTime {T : Type u} {R : Type v} [CommSemiring R] {S : Type w} (f : S → T) (X : AlgebraicBranchedRoughPath T R) (s t : S) (τ : HopfAlgebras.RootedTree) : (comapTime f X).treeCoeff s t τ = X.treeCoeff (f s) (f t) τ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.comapTime_id {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) : comapTime id X = X

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

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.comapTime_unit {T : Type u} {R : Type v} [CommSemiring R] {S : Type w} (f : S → T) : comapTime f (unit T R) = unit S R

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.coeff_empty {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : HopfRoughPath.coeff X s t HopfAlgebras.RootedForest.empty = 1

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.coeff_zero {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : HopfRoughPath.coeff X s t 0 = 1

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.coeff_add {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (φ ψ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff X s t (φ + ψ) = HopfRoughPath.coeff X s t φ * HopfRoughPath.coeff X s t ψ

@[reducible, inline]

abbrev RoughPaths.AlgebraicBranchedRoughPath.AgreeUpToOrder {T : Type u} {R : Type v} [CommSemiring R] (X Y : AlgebraicBranchedRoughPath T R) (n : ℕ) : Prop

Two algebraic branched rough paths agree through forest order n.

Equations

• X.AgreeUpToOrder Y n = RoughPaths.HopfRoughPath.AgreeUpTo HopfAlgebras.RootedForest.order X Y n

theorem RoughPaths.AlgebraicBranchedRoughPath.agreeUpToOrder_refl {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (n : ℕ) : X.AgreeUpToOrder X n

theorem RoughPaths.AlgebraicBranchedRoughPath.agreeUpToOrder_iff_coeff {T : Type u} {R : Type v} [CommSemiring R] (X Y : AlgebraicBranchedRoughPath T R) (n : ℕ) : X.AgreeUpToOrder Y n ↔ ∀ (s t : T) (φ : HopfAlgebras.RootedForest), φ.order ≤ n → HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ

theorem RoughPaths.AlgebraicBranchedRoughPath.eq_of_agreeUpToOrder_all {T : Type u} {R : Type v} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} (h : ∀ (n : ℕ), X.AgreeUpToOrder Y n) : X = Y

theorem RoughPaths.AlgebraicBranchedRoughPath.agreeUpToOrder_all_iff_eq {T : Type u} {R : Type v} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} : (∀ (n : ℕ), X.AgreeUpToOrder Y n) ↔ X = Y

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.character_self {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (t : T) : X.character t t = HopfAlgebras.ForestAlgebra.Character.unit R

theorem RoughPaths.AlgebraicBranchedRoughPath.coeff_self {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (t : T) (φ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff X t t φ = HopfAlgebras.ForestAlgebra.counitCoeff φ

theorem RoughPaths.AlgebraicBranchedRoughPath.chen_eq {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t u : T) : X.character s u = (X.character s t).convolution (X.character t u)

Chen's identity for the lifted algebra characters.

theorem RoughPaths.AlgebraicBranchedRoughPath.increment_convolution_reverse {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : (X.character s t).convolution (X.character t s) = HopfAlgebras.ForestAlgebra.Character.unit R

theorem RoughPaths.AlgebraicBranchedRoughPath.reverse_convolution_increment {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : (X.character t s).convolution (X.character s t) = HopfAlgebras.ForestAlgebra.Character.unit R

theorem RoughPaths.AlgebraicBranchedRoughPath.chen_coeff {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t u : T) (φ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff X s u φ = HopfAlgebras.RootedForest.convolutionCoeff (X.character s t) (X.character t u) φ

theorem RoughPaths.AlgebraicBranchedRoughPath.chen_treeCoeff {T : Type u} {R : Type v} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t u : T) (τ : HopfAlgebras.RootedTree) : X.treeCoeff s u τ = HopfAlgebras.RootedTree.convolutionCoeff (X.character s t) (X.character t u) τ

theorem RoughPaths.AlgebraicBranchedRoughPath.unit_coeff {T : Type u} {R : Type v} [CommSemiring R] (s t : T) (φ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff (unit T R) s t φ = HopfAlgebras.ForestAlgebra.counitCoeff φ

@[reducible, inline]

abbrev RoughPaths.AlgebraicLabelledBranchedRoughPath (T : Type u) (α : Type v) (R : Type w) [CommSemiring R] : Type (max u v w)

A labelled branched rough path is a Hopf rough path over the labelled BCK bialgebra of decorated rooted forests.

Equations

• RoughPaths.AlgebraicLabelledBranchedRoughPath T α R = RoughPaths.HopfRoughPath (HopfAlgebras.lbckBialg α) T R

@[reducible, inline]

noncomputable abbrev RoughPaths.AlgebraicLabelledBranchedRoughPath.unit (T : Type u) (α : Type v) (R : Type w) [CommSemiring R] : AlgebraicLabelledBranchedRoughPath T α R

The constant identity labelled branched rough path.

Equations

• RoughPaths.AlgebraicLabelledBranchedRoughPath.unit T α R = RoughPaths.HopfRoughPath.unit (HopfAlgebras.lbckBialg α) T R

@[reducible, inline]

noncomputable abbrev RoughPaths.AlgebraicLabelledBranchedRoughPath.comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : AlgebraicLabelledBranchedRoughPath T α R) : AlgebraicLabelledBranchedRoughPath S α R

Pull a labelled branched rough path back along a map of time domains.

Equations

• RoughPaths.AlgebraicLabelledBranchedRoughPath.comapTime f X = RoughPaths.HopfRoughPath.comapTime f X

@[simp]

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.treeCoeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (τ : HopfAlgebras.LRootedTree α) : R

Coordinate of an increment on a labelled rooted tree.

Equations

• X.treeCoeff s t τ = RoughPaths.HopfRoughPath.coeff X s t (HopfAlgebras.LRootedForest.singleton τ)

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.lcharacter {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : HopfAlgebras.LForestAlgebra.Character α R

The increment as an algebra character of the labelled forest algebra, via the AddMonoidAlgebra.lift bridge lbckCharacter.

Equations

• X.lcharacter s t = HopfAlgebras.lbckCharacter ↑(X.increment s t) ⋯

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.lcharacter_evalForest {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (φ : HopfAlgebras.LRootedForest α) : (X.lcharacter s t).evalForest φ = HopfRoughPath.coeff X s t φ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.lcharacter_self {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (t : T) : X.lcharacter t t = HopfAlgebras.LForestAlgebra.Character.unit α R

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.lchen_eq {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t u : T) : X.lcharacter s u = (X.lcharacter s t).convolution (X.lcharacter t u)

Chen's identity for the lifted labelled algebra characters.

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) : AlgebraicLabelledBranchedRoughPath T α R

Pull a labelled branched rough path back along a relabelling map.

Equations

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

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff (comapMapLabels f X) s t φ = HopfRoughPath.coeff X s t (HopfAlgebras.LRootedForest.mapLabels f φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.ext {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} (h : ∀ (s t : T) (φ : HopfAlgebras.LRootedForest α), HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ) : X = Y

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.ext_iff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} : X = Y ↔ ∀ (s t : T) (φ : HopfAlgebras.LRootedForest α), HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : S) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff (comapTime f X) s t φ = HopfRoughPath.coeff X (f s) (f t) φ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.treeCoeff_comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : S) (τ : HopfAlgebras.LRootedTree α) : (comapTime f X).treeCoeff s t τ = X.treeCoeff (f s) (f t) τ

@[simp]

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

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

@[simp]

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

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_empty {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : HopfRoughPath.coeff X s t HopfAlgebras.LRootedForest.empty = 1

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_zero {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : HopfRoughPath.coeff X s t 0 = 1

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_add {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (φ ψ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff X s t (φ + ψ) = HopfRoughPath.coeff X s t φ * HopfRoughPath.coeff X s t ψ

@[reducible, inline]

abbrev RoughPaths.AlgebraicLabelledBranchedRoughPath.AgreeUpToOrder {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X Y : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) : Prop

Two algebraic labelled branched rough paths agree through forest order n.

Equations

• X.AgreeUpToOrder Y n = RoughPaths.HopfRoughPath.AgreeUpTo HopfAlgebras.LRootedForest.order X Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_refl {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) : X.AgreeUpToOrder X n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_iff_coeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X Y : AlgebraicLabelledBranchedRoughPath T α R) (n : ℕ) : X.AgreeUpToOrder Y n ↔ ∀ (s t : T) (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff Y s t φ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.eq_of_agreeUpToOrder_all {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} (h : ∀ (n : ℕ), X.AgreeUpToOrder Y n) : X = Y

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_all_iff_eq {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} : (∀ (n : ℕ), X.AgreeUpToOrder Y n) ↔ X = Y

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.AgreeUpToOrder.comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) {X Y : AlgebraicLabelledBranchedRoughPath T β R} {n : ℕ} (h : X.AgreeUpToOrder Y n) : (AlgebraicLabelledBranchedRoughPath.comapMapLabels f X).AgreeUpToOrder (AlgebraicLabelledBranchedRoughPath.comapMapLabels f Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.treeCoeff_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) (τ : HopfAlgebras.LRootedTree α) : (comapMapLabels f X).treeCoeff s t τ = X.treeCoeff s t (HopfAlgebras.LRootedTree.map f τ)

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapMapLabels_id {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) : comapMapLabels id X = X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapMapLabels_comp {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} {γ : Type y} (f : α → β) (g : β → γ) (X : AlgebraicLabelledBranchedRoughPath T γ R) : comapMapLabels f (comapMapLabels g X) = comapMapLabels (g ∘ f) X

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapMapLabels_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) : comapMapLabels f (unit T β R) = unit T α R

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) : AlgebraicLabelledBranchedRoughPath T α R

Pull an unlabelled branched rough path back by forgetting labels.

Equations

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) : AlgebraicBranchedRoughPath T R

Pull a labelled branched rough path back along constant labelling.

Equations

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

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff (comapEraseLabels X) s t φ = HopfRoughPath.coeff X s t φ.erase

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.AgreeUpToOrder.comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} {n : ℕ} (h : X.AgreeUpToOrder Y n) : (AlgebraicLabelledBranchedRoughPath.comapEraseLabels X).AgreeUpToOrder (AlgebraicLabelledBranchedRoughPath.comapEraseLabels Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.treeCoeff_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (τ : HopfAlgebras.LRootedTree α) : (comapEraseLabels X).treeCoeff s t τ = X.treeCoeff s t τ.erase

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (φ : HopfAlgebras.RootedForest) : HopfRoughPath.coeff (comapConstLabel a X) s t φ = HopfRoughPath.coeff X s t (HopfAlgebras.LRootedForest.constLabel a φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.AgreeUpToOrder.comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) {X Y : AlgebraicLabelledBranchedRoughPath T α R} {n : ℕ} (h : X.AgreeUpToOrder Y n) : (AlgebraicLabelledBranchedRoughPath.comapConstLabel a X).AgreeUpToOrder (AlgebraicLabelledBranchedRoughPath.comapConstLabel a Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.treeCoeff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (τ : HopfAlgebras.RootedTree) : (comapConstLabel a X).treeCoeff s t τ = X.treeCoeff s t (HopfAlgebras.LRootedTree.constLabel a τ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapConstLabel_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) (X : AlgebraicBranchedRoughPath T R) : comapConstLabel a (comapEraseLabels X) = X

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapEraseLabels_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] : comapEraseLabels (AlgebraicBranchedRoughPath.unit T R) = unit T α R

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.comapConstLabel_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) : comapConstLabel a (unit T α R) = AlgebraicBranchedRoughPath.unit T R

def RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) : Prop

A labelled branched rough path whose increments only depend on unlabelled forests.

Equations

• X.LabelInvariant = ∀ (s t : T), (X.lcharacter s t).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.lcharacter {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} (h : X.LabelInvariant) (s t : T) : (X.lcharacter s t).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.coeff_eq {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} (h : X.LabelInvariant) {s t : T} {φ ψ : HopfAlgebras.LRootedForest α} (hφψ : φ.erase = ψ.erase) : HopfRoughPath.coeff X s t φ = HopfRoughPath.coeff X s t ψ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.lcharacter_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : (comapEraseLabels X).lcharacter s t = HopfAlgebras.LForestAlgebra.Character.comapEraseLabels (X.character s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.lcharacter_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) : (comapMapLabels f X).lcharacter s t = HopfAlgebras.LForestAlgebra.Character.comapMapLabels f (X.lcharacter s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.character_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : (comapConstLabel a X).character s t = HopfAlgebras.LForestAlgebra.Character.comapConstLabel a (X.lcharacter s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariant_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) : (comapEraseLabels X).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariant_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] : (unit T α R).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.comapMapLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} {X : AlgebraicLabelledBranchedRoughPath T β R} (h : X.LabelInvariant) (f : α → β) : (AlgebraicLabelledBranchedRoughPath.comapMapLabels f X).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.comapConstLabel_eq {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} (h : X.LabelInvariant) (x y : α) : comapConstLabel x X = comapConstLabel y X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.comapEraseLabels_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} (h : X.LabelInvariant) (x : α) : comapEraseLabels (comapConstLabel x X) = X

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] : AlgebraicBranchedRoughPath T R ≃ { X : AlgebraicLabelledBranchedRoughPath T α R // X.LabelInvariant }

Unlabelled branched rough paths are equivalent to label-invariant labelled ones.

Equations

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

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_apply {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] (X : AlgebraicBranchedRoughPath T R) : ↑(labelInvariantEquiv X) = comapEraseLabels X

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_symm_apply {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] (X : { X : AlgebraicLabelledBranchedRoughPath T α R // X.LabelInvariant }) : labelInvariantEquiv.symm X = comapConstLabel (Classical.choice ⋯) ↑X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] : labelInvariantEquiv (AlgebraicBranchedRoughPath.unit T R) = ⟨unit T α R, ⋯⟩

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_symm_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] : labelInvariantEquiv.symm ⟨unit T α R, ⋯⟩ = AlgebraicBranchedRoughPath.unit T R

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariant_iff_exists_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] (X : AlgebraicLabelledBranchedRoughPath T α R) : X.LabelInvariant ↔ ∃ (Y : AlgebraicBranchedRoughPath T R), comapEraseLabels Y = X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_of_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicBranchedRoughPath T R} {n : ℕ} (x : α) (h : (comapEraseLabels X).AgreeUpToOrder (comapEraseLabels Y) n) : X.AgreeUpToOrder Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_comapEraseLabels_iff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : AlgebraicBranchedRoughPath T R} {n : ℕ} : (comapEraseLabels X).AgreeUpToOrder (comapEraseLabels Y) n ↔ X.AgreeUpToOrder Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.agreeUpToOrder_all_comapEraseLabels_iff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : AlgebraicBranchedRoughPath T R} : (∀ (n : ℕ), (comapEraseLabels X).AgreeUpToOrder (comapEraseLabels Y) n) ↔ ∀ (n : ℕ), X.AgreeUpToOrder Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.agreeUpToOrder_iff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} {n : ℕ} (hX : X.LabelInvariant) (hY : Y.LabelInvariant) (x : α) : X.AgreeUpToOrder Y n ↔ (comapConstLabel x X).AgreeUpToOrder (comapConstLabel x Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.LabelInvariant.agreeUpToOrder_all_iff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} (hX : X.LabelInvariant) (hY : Y.LabelInvariant) (x : α) : (∀ (n : ℕ), X.AgreeUpToOrder Y n) ↔ ∀ (n : ℕ), (comapConstLabel x X).AgreeUpToOrder (comapConstLabel x Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_agreeUpToOrder {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : AlgebraicBranchedRoughPath T R} {n : ℕ} : (↑(labelInvariantEquiv X)).AgreeUpToOrder (↑(labelInvariantEquiv Y)) n ↔ X.AgreeUpToOrder Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_symm_agreeUpToOrder {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : { X : AlgebraicLabelledBranchedRoughPath T α R // X.LabelInvariant }} {n : ℕ} : (labelInvariantEquiv.symm X).AgreeUpToOrder (labelInvariantEquiv.symm Y) n ↔ (↑X).AgreeUpToOrder (↑Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_agreeUpToOrder_all {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : AlgebraicBranchedRoughPath T R} : (∀ (n : ℕ), (↑(labelInvariantEquiv X)).AgreeUpToOrder (↑(labelInvariantEquiv Y)) n) ↔ ∀ (n : ℕ), X.AgreeUpToOrder Y n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.labelInvariantEquiv_symm_agreeUpToOrder_all {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] [Nonempty α] {X Y : { X : AlgebraicLabelledBranchedRoughPath T α R // X.LabelInvariant }} : (∀ (n : ℕ), (labelInvariantEquiv.symm X).AgreeUpToOrder (labelInvariantEquiv.symm Y) n) ↔ ∀ (n : ℕ), (↑X).AgreeUpToOrder (↑Y) n

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.coeff_self {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (t : T) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff X t t φ = HopfAlgebras.LForestAlgebra.counitCoeff φ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.increment_convolution_reverse {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : (X.lcharacter s t).convolution (X.lcharacter t s) = HopfAlgebras.LForestAlgebra.Character.unit α R

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.reverse_convolution_increment {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) : (X.lcharacter t s).convolution (X.lcharacter s t) = HopfAlgebras.LForestAlgebra.Character.unit α R

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.chen_coeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t u : T) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff X s u φ = HopfAlgebras.LRootedForest.convolutionCoeff (X.lcharacter s t) (X.lcharacter t u) φ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.chen_treeCoeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t u : T) (τ : HopfAlgebras.LRootedTree α) : X.treeCoeff s u τ = HopfAlgebras.LRootedTree.convolutionCoeff (X.lcharacter s t) (X.lcharacter t u) τ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.unit_coeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (s t : T) (φ : HopfAlgebras.LRootedForest α) : HopfRoughPath.coeff (unit T α R) s t φ = HopfAlgebras.LForestAlgebra.counitCoeff φ