The branched rough integral (level 2)

Gubinelli's controlled integration against a branched rough path (Gubinelli, Ramification of rough paths, math/0610300 §7–8), at level 2 over unlabelled trees: the only trees of order at most two are • and the 2-chain, so a level-2 branched rough path is the data (X^•, X^chain2) and Chen's identity for the Butcher–Connes–Kreimer convolution reduces on them to the classical relations X^•(s,u) = X^•(s,t) + X^•(t,u) and X^ch(s,u) = X^ch(s,t) + X^•(s,t)·X^•(t,u) + X^ch(t,u). The germ Ξ s t = X^•(s,t)·Y(s) + X^ch(s,t)·Y'(s) then has defect of order ω^{3α} and sews into the branched rough integral. Since only Chen's identity is used, non-geometric branched (Itô-type) data is covered.

Chen's identity on trees of order at most two

theorem RoughPaths.AlgebraicBranchedRoughPath.chen_treeCoeff_bullet {T : Type u_2} {R : Type u_3} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t u : T) : X.treeCoeff s u HopfAlgebras.RootedTree.bullet = X.treeCoeff s t HopfAlgebras.RootedTree.bullet + X.treeCoeff t u HopfAlgebras.RootedTree.bullet

Chen's identity at the single-node tree: the first level is additive.

theorem RoughPaths.AlgebraicBranchedRoughPath.chen_treeCoeff_chain2 {T : Type u_2} {R : Type u_3} [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (s t u : T) : X.treeCoeff s u HopfAlgebras.RootedTree.chain2 = X.treeCoeff s t HopfAlgebras.RootedTree.chain2 + X.treeCoeff s t HopfAlgebras.RootedTree.bullet * X.treeCoeff t u HopfAlgebras.RootedTree.bullet + X.treeCoeff t u HopfAlgebras.RootedTree.chain2

Chen's identity at the 2-chain: the classical level-2 relation.

Level-2 branched rough paths and controlled paths

structure RoughPaths.IsLevel2BranchedRoughPath (X : AlgebraicBranchedRoughPath ℝ ℝ) (ω : Control ℝ) (α : ℝ) : Prop

Level-2 Hölder-type bounds for a real branched rough path: the single-node coefficient of order ω^α, the 2-chain of order ω^{2α}.

• one_third_lt : 1 / 3 < α
• le_half : α ≤ 1 / 2
• bound_bullet ⦃s t : ℝ⦄ : s ≤ t → ‖X.treeCoeff s t HopfAlgebras.RootedTree.bullet‖ₑ ≤ ω.toFun s t ^ α
• bound_chain2 ⦃s t : ℝ⦄ : s ≤ t → ‖X.treeCoeff s t HopfAlgebras.RootedTree.chain2‖ₑ ≤ ω.toFun s t ^ (2 * α)

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

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

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

A path controlled by a level-2 branched rough path: a Gubinelli derivative along the single-node coefficient with ω^{2α} remainder.

• Y : ℝ → W

  The underlying path.

• Yd : ℝ → W

  The Gubinelli derivative.

• Cb : NNReal

  Sup bound for the derivative.

• Cd : NNReal

  Hölder constant of the derivative.

• Cy : NNReal

  Remainder constant.

• bound_Yd (s : ℝ) : ‖self.Yd s‖ₑ ≤ ↑self.Cb
• holder_Yd ⦃s t : ℝ⦄ : s ≤ t → ‖self.Yd t - self.Yd s‖ₑ ≤ ↑self.Cd * ω.toFun s t ^ α
• remainder ⦃s t : ℝ⦄ : s ≤ t → ‖self.Y t - self.Y s - X.treeCoeff s t HopfAlgebras.RootedTree.bullet • self.Yd s‖ₑ ≤ ↑self.Cy * ω.toFun s t ^ (2 * α)

The branched Gubinelli germ

noncomputable def RoughPaths.branchedGerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : BranchedControlledPath X ω α E) : ℝ → ℝ → E

The branched Gubinelli germ: the two-term local expansion of ∫_s^t Y dX^• using the 2-chain as second-level data.

Equations

• RoughPaths.branchedGerm Z s t = X.treeCoeff s t HopfAlgebras.RootedTree.bullet • Z.Y s + X.treeCoeff s t HopfAlgebras.RootedTree.chain2 • Z.Yd s

theorem RoughPaths.branchedGerm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : BranchedControlledPath X ω α E) (s t : ℝ) : branchedGerm Z s t = X.treeCoeff s t HopfAlgebras.RootedTree.bullet • Z.Y s + X.treeCoeff s t HopfAlgebras.RootedTree.chain2 • Z.Yd s

theorem RoughPaths.branchedGerm_defect_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (Z : BranchedControlledPath X ω α E) (a b c : ℝ) : branchedGerm Z a c - branchedGerm Z a b - branchedGerm Z b c = X.treeCoeff b c HopfAlgebras.RootedTree.bullet • (Z.Y a - Z.Y b + X.treeCoeff a b HopfAlgebras.RootedTree.bullet • Z.Yd a) + X.treeCoeff b c HopfAlgebras.RootedTree.chain2 • (Z.Yd a - Z.Yd b)

The algebraic defect identity from Chen's relations on small trees.

theorem RoughPaths.branchedGerm_defect {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2BranchedRoughPath X ω α) (Z : BranchedControlledPath X ω α E) ⦃a b c : ℝ⦄ : a ≤ b → b ≤ c → ‖branchedGerm Z a c - branchedGerm Z a b - branchedGerm Z b c‖ₑ ≤ (↑Z.Cy + ↑Z.Cd) * ω.toFun a c ^ (3 * α)

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

Existence and uniqueness of the branched rough integral

theorem RoughPaths.exists_branchedRoughIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (hX : IsLevel2BranchedRoughPath X ω α) (Z : BranchedControlledPath 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 - branchedGerm Z s t‖ₑ ≤ Sewing.sewingConst (3 * α) * ((↑Z.Cy + ↑Z.Cd) * ω.toFun s t ^ (3 * α))) ∧ ∀ ⦃s t : ℝ⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List ℝ), List.IsChain (fun (a b : ℝ) => a ≤ b ∧ (Control.constMul ((↑Z.Cy + ↑Z.Cd) ^ (3 * α)⁻¹) ω).toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - Sewing.pairSum (branchedGerm Z) (s :: (mid ++ [t]))‖ₑ ≤ Sewing.sewingConst (3 * α) * (ε ^ (3 * α - 1) * (Control.constMul ((↑Z.Cy + ↑Z.Cd) ^ (3 * α)⁻¹) ω).toFun s t)

Existence of the branched rough integral (Gubinelli math/0610300, level-2 case): an additive ∫ Y dX with germ estimate of order ω^{3α}, approximating compensated Riemann sums of fine partitions.

theorem RoughPaths.branchedRoughIntegral_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2BranchedRoughPath X ω α) (Z : BranchedControlledPath 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 - branchedGerm Z a b‖ₑ ≤ C * ω.toFun a b ^ (3 * α)) (hI' : ∀ ⦃a b : ℝ⦄, a ≤ b → ‖I' a b - branchedGerm 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 branched rough integral among additive maps with a germ bound of order 3α > 1.

theorem RoughPaths.branchedRoughIntegral_sub_linear {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicBranchedRoughPath ℝ ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2BranchedRoughPath X ω α) (Z : BranchedControlledPath X ω α E) {I : ℝ → ℝ → E} (hgerm : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I s t - branchedGerm Z s t‖ₑ ≤ Sewing.sewingConst (3 * α) * ((↑Z.Cy + ↑Z.Cd) * ω.toFun s t ^ (3 * α))) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖I s t - X.treeCoeff s t HopfAlgebras.RootedTree.bullet • Z.Y s‖ₑ ≤ Sewing.sewingConst (3 * α) * ((↑Z.Cy + ↑Z.Cd) * ω.toFun s t ^ (3 * α)) + ↑Z.Cb * ω.toFun s t ^ (2 * α)

The branched rough integral is controlled with Gubinelli derivative Y: subtracting the first-level part leaves ω^{2α} order plus the sewing error.