The three instances of Hopf rough paths

The abstract HopfRoughPath (Rahm, Definition 2.2) specialises to the three signature notions of the library, with inverse translations:

• classical: weakly geometric word rough paths over the shuffle Hopf algebra — AlgebraicRoughPath.toHopf / HopfRoughPath.toWord;
• branched: AlgebraicBranchedRoughPath is defined as HopfRoughPath bckBialg (RoughPaths.Branched) — no bridge needed;
• planar branched: PlanarBranchedRoughPath is defined as HopfRoughPath mkwBialg (RoughPaths.PlanarBranched) — no bridge needed.

The γ-regularity of Definition 2.2.3 specialises with the natural gradings: word length, forest order, and planar forest order.

Classical rough paths: the word shuffle Hopf algebra

def RoughPaths.AlgebraicRoughPath.toHopf {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicRoughPath T α R) (hX : X.IsWeaklyGeometric) : HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg T R

A weakly geometric word rough path is a Hopf rough path over the word shuffle Hopf algebra.

Equations

• X.toHopf hX = { increment := fun (s t : T) => ⟨X.increment s t, ⋯⟩, identity := ⋯, chen := ⋯ }

def RoughPaths.HopfRoughPath.toWord {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg T R) : AlgebraicRoughPath T α R

A Hopf rough path over the word shuffle Hopf algebra is a (weakly geometric) word rough path.

Equations

• X.toWord = { increment := fun (s t : T) => ↑(X.increment s t), identity := ⋯, chen := ⋯, unitEmpty := ⋯ }

theorem RoughPaths.HopfRoughPath.toWord_isWeaklyGeometric {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg T R) : X.toWord.IsWeaklyGeometric

@[simp]

theorem RoughPaths.AlgebraicRoughPath.toHopf_toWord {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicRoughPath T α R) (hX : X.IsWeaklyGeometric) : (X.toHopf hX).toWord = X

@[simp]

theorem RoughPaths.HopfRoughPath.toWord_toHopf {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg T R) : X.toWord.toHopf ⋯ = X

γ-regularity with the natural gradings (Definition 2.2.3)

@[reducible, inline]

abbrev RoughPaths.HopfRoughPath.IsGeometricHolder {α : Type} (X : HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg ℝ ℝ) (γ : ℝ) : Prop

A γ-regular classical rough path: Definition 2.2 over the word shuffle Hopf algebra, graded by word length.

Equations

• X.IsGeometricHolder γ = X.IsHolderRegular List.length γ

@[reducible, inline]

abbrev RoughPaths.HopfRoughPath.IsBranchedHolder (X : HopfRoughPath HopfAlgebras.bckBialg ℝ ℝ) (γ : ℝ) : Prop

A γ-regular branched rough path: Definition 2.2 over the BCK bialgebra, graded by forest order.

Equations

• X.IsBranchedHolder γ = X.IsHolderRegular HopfAlgebras.RootedForest.order γ

@[reducible, inline]

abbrev RoughPaths.HopfRoughPath.IsPlanarBranchedHolder (X : HopfRoughPath HopfAlgebras.mkwBialg ℝ ℝ) (γ : ℝ) : Prop

A γ-regular planarly branched rough path: Definition 2.2 over the MKW bialgebra, graded by planar forest order.

Equations

• X.IsPlanarBranchedHolder γ = X.IsHolderRegular HopfAlgebras.PlanarForest.order γ