Rough paths over a combinatorial Hopf algebra

The abstract H-rough path of L. Rahm, Planar Regularity Structures (Found. Comput. Math. 2026), Definition 2.2: a two-parameter family of characters of a combinatorial (Hopf) bialgebra H, equal to the counit on the diagonal and satisfying Chen's identity — the increment over [s, u] is the convolution of the increments over [s, t] and [t, u]. In our character monoid this is simply

• increment t t = 1, and
• increment s u = increment s t * increment t u.

This single structure subsumes classical (weakly geometric) rough paths (H = wordHopf, the shuffle algebra of words), branched rough paths (H = bckBialg, Butcher–Connes–Kreimer) and planarly branched rough paths (H = mkwBialg, Munthe-Kaas–Wright) — the identifications are in RoughPaths.HopfRoughPathInstances.

The theory shared by all instances is proved here once:

• coefficient-level Chen expansion (chen_coeff), unit and multiplicativity of coefficients;
• the constant unit rough path and time reparametrisation;
• increments are units of the character monoid: the reverse increment is a two-sided convolution inverse, purely from Chen and the diagonal identity — no antipode needed (increment_mul_reverse); over a genuine Hopf algebra the reverse increment is the group inverse, i.e. antipode precomposition (increment_reverse_eq_inv);
• Chen along a chain of intermediate times (increment_eq_prod);
• agreement up to a degree, for any grading of the basis (AgreeUpTo);
• γ-regularity in the sense of Definition 2.2.3: every graded basis coefficient is γ·deg-Hölder (IsHolderRegular).

structure RoughPaths.HopfRoughPath {B : Type u} (H : HopfAlgebras.CombBialg B) (T : Type w) (R : Type v) [CommSemiring R] : Type (max (max u v) w)

A rough path over a combinatorial Hopf algebra H (Rahm, Definition 2.2, algebraic part): a two-parameter family of characters of H which is the counit on the diagonal and satisfies Chen's identity, i.e. a multiplicative two-parameter family in the character monoid of H.

• increment : T → T → H.Character R

  The increment character over the interval [s, t].

• identity (t : T) : self.increment t t = 1

  Diagonal increments are the convolution unit (the counit).

• chen (s t u : T) : self.increment s u = self.increment s t * self.increment t u

  Chen's identity: convolution of adjacent increments.

def RoughPaths.HopfRoughPath.coeff {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) (x : B) : R

The coefficient of a basis element in an increment.

Equations

• X.coeff s t x = ↑(X.increment s t) x

@[simp]

theorem RoughPaths.HopfRoughPath.coeff_apply {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) (x : B) : X.coeff s t x = ↑(X.increment s t) x

theorem RoughPaths.HopfRoughPath.ext {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {X Y : HopfRoughPath H T R} (h : ∀ (s t : T), X.increment s t = Y.increment s t) : X = Y

theorem RoughPaths.HopfRoughPath.ext_iff {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {X Y : HopfRoughPath H T R} : X = Y ↔ ∀ (s t : T), X.increment s t = Y.increment s t

theorem RoughPaths.HopfRoughPath.ext_coeff {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {X Y : HopfRoughPath H T R} (h : ∀ (s t : T) (x : B), X.coeff s t x = Y.coeff s t x) : X = Y

@[simp]

theorem RoughPaths.HopfRoughPath.coeff_one {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) : X.coeff s t H.one = 1

The coefficient of the unit basis element is 1 — the increments are normalized linear forms.

theorem RoughPaths.HopfRoughPath.coeff_mul {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) (x y : B) : X.coeff s t x * X.coeff s t y = (List.map (X.coeff s t) (H.mul x y)).sum

Increments are multiplicative on basis products — the linear forms are characters (Definition 2.2.1).

theorem RoughPaths.HopfRoughPath.coeff_mul_single {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) {x y z : B} (h : H.mul x y = [z]) (s t : T) : X.coeff s t z = X.coeff s t x * X.coeff s t y

For a monomial product expansion mul x y = [z] — as in the BCK and MKW forest bialgebras — coefficients are multiplicative on the product: ⟨X, z⟩ = ⟨X, x⟩·⟨X, y⟩.

theorem RoughPaths.HopfRoughPath.coeff_diagonal {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (t : T) (x : B) : X.coeff t t x = if H.isOne x = true then 1 else 0

Diagonal coefficients are the counit.

theorem RoughPaths.HopfRoughPath.chen_coeff {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t u : T) (x : B) : X.coeff s u x = (List.map (fun (p : B × B) => X.coeff s t p.1 * X.coeff t u p.2) (H.coprod x)).sum

Chen's identity at the level of coefficients: the coproduct expansion of the increment over [s, u] (Definition 2.2.2).

The unit rough path and reparametrisation

noncomputable def RoughPaths.HopfRoughPath.unit {B : Type u} (H : HopfAlgebras.CombBialg B) (T : Type w) (R : Type v) [CommSemiring R] : HopfRoughPath H T R

The constant unit rough path: every increment is the counit.

Equations

• RoughPaths.HopfRoughPath.unit H T R = { increment := fun (x x_1 : T) => 1, identity := ⋯, chen := ⋯ }

@[simp]

theorem RoughPaths.HopfRoughPath.unit_increment {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (s t : T) : (unit H T R).increment s t = 1

theorem RoughPaths.HopfRoughPath.unit_coeff {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (s t : T) (x : B) : (unit H T R).coeff s t x = if H.isOne x = true then 1 else 0

def RoughPaths.HopfRoughPath.comapTime {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {S : Type z} (f : S → T) (X : HopfRoughPath H T R) : HopfRoughPath H S R

Reparametrise time along a map f : S → T.

Equations

• RoughPaths.HopfRoughPath.comapTime f X = { increment := fun (s t : S) => X.increment (f s) (f t), identity := ⋯, chen := ⋯ }

@[simp]

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

@[simp]

theorem RoughPaths.HopfRoughPath.coeff_comapTime {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {S : Type z} (f : S → T) (X : HopfRoughPath H T R) (s t : S) (x : B) : (comapTime f X).coeff s t x = X.coeff (f s) (f t) x

theorem RoughPaths.HopfRoughPath.comapTime_id {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) : comapTime id X = X

theorem RoughPaths.HopfRoughPath.comapTime_comp {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {S U : Type z} (f : S → T) (g : U → S) (X : HopfRoughPath H T R) : comapTime g (comapTime f X) = comapTime (f ∘ g) X

theorem RoughPaths.HopfRoughPath.comapTime_unit {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {S : Type z} (f : S → T) : comapTime f (unit H T R) = unit H S R

Increments are units of the character monoid

The reverse increment is a two-sided convolution inverse, purely from Chen's identity and the diagonal condition — no antipode is needed.

theorem RoughPaths.HopfRoughPath.increment_mul_reverse {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) : X.increment s t * X.increment t s = 1

theorem RoughPaths.HopfRoughPath.reverse_mul_increment {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) : X.increment t s * X.increment s t = 1

theorem RoughPaths.HopfRoughPath.isUnit_increment {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (s t : T) : IsUnit (X.increment s t)

theorem RoughPaths.HopfRoughPath.increment_reverse_eq_inv {B : Type u} {T : Type w} {H : HopfAlgebras.CombHopf B} {R' : Type v} [CommRing R'] (X : HopfRoughPath H.toCombBialg T R') (s t : T) : X.increment t s = (X.increment s t)⁻¹

Over a genuine Hopf algebra the reverse increment is the group inverse of the character group — precomposition with the antipode.

Chen along a chain

theorem RoughPaths.HopfRoughPath.increment_eq_prod {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (X : HopfRoughPath H T R) (mid : List T) (s t : T) : X.increment s t = (List.map (fun (q : T × T) => X.increment q.1 q.2) ((s :: mid).zip (mid ++ [t]))).prod

Chen's identity along a chain of intermediate times: the increment over [s, t] is the ordered convolution product of the increments along s, p₁, …, pₙ, t.

Agreement up to a degree

def RoughPaths.HopfRoughPath.AgreeUpTo {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (deg : B → ℕ) (X Y : HopfRoughPath H T R) (n : ℕ) : Prop

Two Hopf rough paths agree up to degree n, with respect to a grading deg of the basis.

Equations

• RoughPaths.HopfRoughPath.AgreeUpTo deg X Y n = ∀ (s t : T) (x : B), deg x ≤ n → X.coeff s t x = Y.coeff s t x

theorem RoughPaths.HopfRoughPath.agreeUpTo_refl {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] (deg : B → ℕ) (X : HopfRoughPath H T R) (n : ℕ) : AgreeUpTo deg X X n

theorem RoughPaths.HopfRoughPath.AgreeUpTo.symm {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {deg : B → ℕ} {X Y : HopfRoughPath H T R} {n : ℕ} (h : AgreeUpTo deg X Y n) : AgreeUpTo deg Y X n

theorem RoughPaths.HopfRoughPath.AgreeUpTo.trans {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {deg : B → ℕ} {X Y Z : HopfRoughPath H T R} {n : ℕ} (h₁ : AgreeUpTo deg X Y n) (h₂ : AgreeUpTo deg Y Z n) : AgreeUpTo deg X Z n

theorem RoughPaths.HopfRoughPath.AgreeUpTo.mono {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {deg : B → ℕ} {X Y : HopfRoughPath H T R} {m n : ℕ} (hmn : m ≤ n) (h : AgreeUpTo deg X Y n) : AgreeUpTo deg X Y m

theorem RoughPaths.HopfRoughPath.AgreeUpTo.comapTime {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {S : Type z} {deg : B → ℕ} {X Y : HopfRoughPath H T R} {n : ℕ} (f : S → T) (h : AgreeUpTo deg X Y n) : AgreeUpTo deg (HopfRoughPath.comapTime f X) (HopfRoughPath.comapTime f Y) n

theorem RoughPaths.HopfRoughPath.eq_of_agreeUpTo_all {B : Type u} {H : HopfAlgebras.CombBialg B} {T : Type w} {R : Type v} [CommSemiring R] {deg : B → ℕ} {X Y : HopfRoughPath H T R} (h : ∀ (n : ℕ), AgreeUpTo deg X Y n) : X = Y

γ-regularity (Definition 2.2.3)

def RoughPaths.HopfRoughPath.IsHolderRegular {B₀ : Type u} {H₀ : HopfAlgebras.CombBialg B₀} (X : HopfRoughPath H₀ ℝ ℝ) (deg : B₀ → ℕ) (γ : ℝ) : Prop

A Hopf rough path over the real line is γ-regular for a grading deg of the basis when every basis coefficient is γ·deg-Hölder: |⟨X_{st}, x⟩| ≤ C_x·|t - s|^{γ·|x|}. This is condition 3 of Definition 2.2 (the finite-supremum form, stated as the existence of a constant per basis element).

Equations

• X.IsHolderRegular deg γ = ∀ (x : B₀), ∃ (C : ℝ), ∀ (s t : ℝ), |X.coeff s t x| ≤ C * |t - s| ^ (γ * ↑(deg x))

theorem RoughPaths.HopfRoughPath.unit_isHolderRegular {B₀ : Type u} {H₀ : HopfAlgebras.CombBialg B₀} {deg : B₀ → ℕ} (h1 : deg H₀.one = 0) (γ : ℝ) : (unit H₀ ℝ ℝ).IsHolderRegular deg γ

The unit rough path is γ-regular for every grading that puts the unit basis element in degree zero.

theorem RoughPaths.HopfRoughPath.IsHolderRegular.comapTime {B₀ : Type u} {H₀ : HopfAlgebras.CombBialg B₀} {X : HopfRoughPath H₀ ℝ ℝ} {deg : B₀ → ℕ} {γ : ℝ} (hγ : 0 ≤ γ) (f : ℝ → ℝ) (hf : ∀ (s t : ℝ), |f t - f s| ≤ |t - s|) (h : X.IsHolderRegular deg γ) : (HopfRoughPath.comapTime f X).IsHolderRegular deg γ

γ-regularity is inherited along contracting reparametrisations of the line; in particular it is invariant under restriction.