Planarly branched rough paths via the MKW Hopf algebra

Planarly branched rough paths (Curry–Ebrahimi-Fard–Manchon–Munthe-Kaas, Planarly branched rough paths and rough differential equations on homogeneous spaces) are defined as Hopf rough paths over the MKW bialgebra: increments are characters of mkwBialg — equivalently, shuffle characters on ordered forests (isShuffleCharacter_iff_isCharacter) — and Chen's identity is convolution in the character monoid, i.e. the Grossman–Larson convolution dual to the Munthe-Kaas–Wright coproduct (mkwConvolution_eq_conv). The generic theory (unit path, time reparametrisation, reverse increments, coefficient Chen) comes from RoughPaths.HopfRoughPath.

At level 2 the ordered forests of order at most two are [•], [chain2] and [•,•], and the MKW coproduct on them yields the Chen relations X^{[•]}(s,u) = X^{[•]}(s,t) + X^{[•]}(t,u) and X^ω(s,u) = X^ω(s,t) + X^{[•]}(s,t)·X^{[•]}(t,u) + X^ω(t,u) for ω ∈ {[chain2], [•,•]}. The controlled-path germ Ξ = X^{[•]}·Y + X^{[chain2]}·Y' + X^{[•,•]}·Y'' therefore has defect of order ω^{3α} — with Gubinelli derivative Y' + Y'' — and sews into the planarly branched rough integral.

Planarly branched rough paths

@[reducible, inline]

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

A planarly branched rough path is a Hopf rough path over the Munthe-Kaas–Wright bialgebra: increments are shuffle characters on ordered forests and Chen's identity is Grossman–Larson convolution.

Equations

• RoughPaths.PlanarBranchedRoughPath T R = RoughPaths.HopfRoughPath HopfAlgebras.mkwBialg T R

theorem RoughPaths.PlanarBranchedRoughPath.isShuffleCharacter {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t : T) : HopfAlgebras.PlanarForest.IsShuffleCharacter ↑(X.increment s t)

Increments are shuffle characters on ordered forests.

@[simp]

theorem RoughPaths.PlanarBranchedRoughPath.coeff_nil {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t : T) : ↑(X.increment s t) [] = 1

theorem RoughPaths.PlanarBranchedRoughPath.counitCoeff_isShuffleCharacter {R : Type v} [CommSemiring R] : HopfAlgebras.PlanarForest.IsShuffleCharacter HopfAlgebras.PlanarForestAlgebra.counitCoeff

The counit is a shuffle character.

theorem RoughPaths.PlanarBranchedRoughPath.chen_coeff {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t u : T) (ω : HopfAlgebras.PlanarForest) : HopfRoughPath.coeff X s u ω = (List.map (fun (pr : HopfAlgebras.PlanarForest × HopfAlgebras.PlanarForest) => HopfRoughPath.coeff X s t pr.1 * HopfRoughPath.coeff X t u pr.2) ω.mkwTerms).sum

Chen's identity in MKW coefficient form.

Chen's identity on forests of order at most two

theorem RoughPaths.PlanarBranchedRoughPath.chen_coeff_bullet {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t u : T) : HopfRoughPath.coeff X s u [HopfAlgebras.PTree.bullet] = HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] + HopfRoughPath.coeff X t u [HopfAlgebras.PTree.bullet]

Chen at the single-bullet forest: additivity of the first level.

theorem RoughPaths.PlanarBranchedRoughPath.chen_coeff_chain2 {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t u : T) : HopfRoughPath.coeff X s u [HopfAlgebras.PTree.chain2] = HopfRoughPath.coeff X s t [HopfAlgebras.PTree.chain2] + HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] * HopfRoughPath.coeff X t u [HopfAlgebras.PTree.bullet] + HopfRoughPath.coeff X t u [HopfAlgebras.PTree.chain2]

Chen at the 2-chain forest.

theorem RoughPaths.PlanarBranchedRoughPath.chen_coeff_bullet_bullet {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t u : T) : HopfRoughPath.coeff X s u [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet] = HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet] + HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] * HopfRoughPath.coeff X t u [HopfAlgebras.PTree.bullet] + HopfRoughPath.coeff X t u [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet]

Chen at the two-bullet forest.

theorem RoughPaths.PlanarBranchedRoughPath.two_mul_coeff_bullet_bullet {T : Type u} {R : Type v} [CommSemiring R] (X : PlanarBranchedRoughPath T R) (s t : T) : 2 * HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet] = HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] * HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet]

For shuffle characters, the two-bullet coefficient is determined by the first level: 2·X^{[•,•]} = (X^{[•]})².

Level-2 analytic bounds and controlled paths

structure RoughPaths.IsLevel2PlanarBranchedRoughPath (X : PlanarBranchedRoughPath ℝ ℝ) (ω : Control ℝ) (α : ℝ) : Prop

Level-2 Hölder-type bounds for a real planarly branched rough path: order-one forests of size ω^α, order-two forests of size ω^{2α}.

• one_third_lt : 1 / 3 < α
• le_half : α ≤ 1 / 2
• bound_bullet ⦃s t : ℝ⦄ : s ≤ t → ‖HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet]‖ₑ ≤ ω.toFun s t ^ α
• bound_chain2 ⦃s t : ℝ⦄ : s ≤ t → ‖HopfRoughPath.coeff X s t [HopfAlgebras.PTree.chain2]‖ₑ ≤ ω.toFun s t ^ (2 * α)
• bound_bullet_bullet ⦃s t : ℝ⦄ : s ≤ t → ‖HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet]‖ₑ ≤ ω.toFun s t ^ (2 * α)

theorem RoughPaths.IsLevel2PlanarBranchedRoughPath.alpha_pos {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2PlanarBranchedRoughPath X ω α) : 0 < α

theorem RoughPaths.IsLevel2PlanarBranchedRoughPath.one_lt_three_alpha {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2PlanarBranchedRoughPath X ω α) : 1 < 3 * α

structure RoughPaths.PlanarControlledPath (X : PlanarBranchedRoughPath ℝ ℝ) (ω : Control ℝ) (α : ℝ) (W : Type u_2) [NormedAddCommGroup W] [NormedSpace ℝ W] : Type u_2

A path controlled by a level-2 planarly branched rough path, with one derivative slot per order-two forest; the Gubinelli derivative pairing the first level is their sum.

• Y : ℝ → W

  The underlying path.

• Yd : ℝ → W

  The derivative slot paired with the 2-chain forest.

• Ye : ℝ → W

  The derivative slot paired with the two-bullet forest.

• Cb : NNReal

  Sup bound for the derivative slots.

• Cd : NNReal

  Hölder constant of the derivative slots.

• Cy : NNReal

  Remainder constant.

• bound_Yd (s : ℝ) : ‖self.Yd s‖ₑ ≤ ↑self.Cb
• bound_Ye (s : ℝ) : ‖self.Ye s‖ₑ ≤ ↑self.Cb
• holder_Yd ⦃s t : ℝ⦄ : s ≤ t → ‖self.Yd t - self.Yd s‖ₑ ≤ ↑self.Cd * ω.toFun s t ^ α
• holder_Ye ⦃s t : ℝ⦄ : s ≤ t → ‖self.Ye t - self.Ye s‖ₑ ≤ ↑self.Cd * ω.toFun s t ^ α
• remainder ⦃s t : ℝ⦄ : s ≤ t → ‖self.Y t - self.Y s - HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] • (self.Yd s + self.Ye s)‖ₑ ≤ ↑self.Cy * ω.toFun s t ^ (2 * α)

The planarly branched Gubinelli germ

noncomputable def RoughPaths.planarGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : PlanarControlledPath X ω α E) : ℝ → ℝ → E

The planarly branched Gubinelli germ: one term per forest of order at most two.

Equations

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

theorem RoughPaths.planarGerm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : PlanarControlledPath X ω α E) (s t : ℝ) : planarGerm Z s t = HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet] • Z.Y s + HopfRoughPath.coeff X s t [HopfAlgebras.PTree.chain2] • Z.Yd s + HopfRoughPath.coeff X s t [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet] • Z.Ye s

theorem RoughPaths.planarGerm_defect_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : PlanarControlledPath X ω α E) (a b c : ℝ) : planarGerm Z a c - planarGerm Z a b - planarGerm Z b c = HopfRoughPath.coeff X b c [HopfAlgebras.PTree.bullet] • (Z.Y a - Z.Y b + HopfRoughPath.coeff X a b [HopfAlgebras.PTree.bullet] • (Z.Yd a + Z.Ye a)) + HopfRoughPath.coeff X b c [HopfAlgebras.PTree.chain2] • (Z.Yd a - Z.Yd b) + HopfRoughPath.coeff X b c [HopfAlgebras.PTree.bullet, HopfAlgebras.PTree.bullet] • (Z.Ye a - Z.Ye b)

The algebraic defect identity from the MKW Chen relations on small forests.

theorem RoughPaths.planarGerm_defect {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2PlanarBranchedRoughPath X ω α) (Z : PlanarControlledPath X ω α E) ⦃a b c : ℝ⦄ : a ≤ b → b ≤ c → ‖planarGerm Z a c - planarGerm Z a b - planarGerm Z b c‖ₑ ≤ (↑Z.Cy + 2 * ↑Z.Cd) * ω.toFun a c ^ (3 * α)

The analytic defect bound: order ω^{3α} with constant Cy + 2·Cd.

Existence and uniqueness of the planarly branched rough

integral

theorem RoughPaths.exists_planarBranchedRoughIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (hX : IsLevel2PlanarBranchedRoughPath X ω α) (Z : PlanarControlledPath X ω α E) (hfine : Sewing.HasFinePartitions ω) (hω : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) : ∃ (I : ℝ → ℝ → E), (∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I s u + I u t = I s t) ∧ (∀ ⦃s t : ℝ⦄, s ≤ t → ‖I s t - planarGerm Z s t‖ₑ ≤ Sewing.sewingConst (3 * α) * ((↑Z.Cy + 2 * ↑Z.Cd) * ω.toFun s t ^ (3 * α))) ∧ ∀ ⦃s t : ℝ⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List ℝ), List.IsChain (fun (a b : ℝ) => a ≤ b ∧ (Control.constMul ((↑Z.Cy + 2 * ↑Z.Cd) ^ (3 * α)⁻¹) ω).toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - Sewing.pairSum (planarGerm Z) (s :: (mid ++ [t]))‖ₑ ≤ Sewing.sewingConst (3 * α) * (ε ^ (3 * α - 1) * (Control.constMul ((↑Z.Cy + 2 * ↑Z.Cd) ^ (3 * α)⁻¹) ω).toFun s t)

Existence of the planarly branched rough integral: an additive ∫ Y dX with germ estimate of order ω^{3α}, approximating compensated Riemann sums of fine partitions.

theorem RoughPaths.planarBranchedRoughIntegral_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : PlanarBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2PlanarBranchedRoughPath X ω α) (Z : PlanarControlledPath X ω α E) {C C' : ENNReal} (hC : C ≠ ⊤) (hC' : C' ≠ ⊤) (hfine : Sewing.HasFinePartitions ω) {I I' : ℝ → ℝ → E} (hadd : ∀ ⦃a u b : ℝ⦄, a ≤ u → u ≤ b → I a u + I u b = I a b) (hadd' : ∀ ⦃a u b : ℝ⦄, a ≤ u → u ≤ b → I' a u + I' u b = I' a b) (hI : ∀ ⦃a b : ℝ⦄, a ≤ b → ‖I a b - planarGerm Z a b‖ₑ ≤ C * ω.toFun a b ^ (3 * α)) (hI' : ∀ ⦃a b : ℝ⦄, a ≤ b → ‖I' a b - planarGerm Z a b‖ₑ ≤ C' * ω.toFun a b ^ (3 * α)) {s t : ℝ} (hst : s ≤ t) (hω : ω.toFun s t ≠ ⊤) : I s t = I' s t

Uniqueness of the planarly branched rough integral among additive maps with a germ bound of order 3α > 1.