The rough integral (level 2)

The Gubinelli germ of a controlled path against a level-2 rough path is Ξ s t = Σᵢ X¹ᵢ(s,t)·Yᵢ(s) + Σᵢⱼ X²ᵢⱼ(s,t)·Y'ᵢⱼ(s). Chen's identity makes its defect δΞ = -Σⱼ X¹ⱼ(u,t)·R_{su}(j) + Σᵢⱼ X²ᵢⱼ(u,t)·(Y'ᵢⱼ(s) - Y'ᵢⱼ(u)), of order ω^{3α} with 3α > 1, so the additive sewing lemma produces the rough integral ∫ Y dX with the local estimate FH (4.21), unique among additive maps with a germ bound of order greater than one, and itself controlled by X with Gubinelli derivative Y. Only Chen's identity is used — non-geometric (Itô-type) rough paths are covered.

References

• P. Friz, M. Hairer, A Course on Rough Paths, Ch. 4
• M. Gubinelli, Controlling rough paths, J. Funct. Anal. 216 (2004)

Chen's identity in level-1 and level-2 coordinates

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_one {T : Type u_2} {α₀ : Type u_3} {R : Type u_4} [Semiring R] (X : AlgebraicRoughPath T α₀ R) (s t u : T) (i : α₀) : X.coeff s u [i] = X.coeff s t [i] + X.coeff t u [i]

theorem RoughPaths.AlgebraicRoughPath.chen_coeff_two {T : Type u_2} {α₀ : Type u_3} {R : Type u_4} [Semiring R] (X : AlgebraicRoughPath T α₀ R) (s t u : T) (i j : α₀) : X.coeff s u [i, j] = X.coeff s t [i, j] + X.coeff s t [i] * X.coeff t u [j] + X.coeff t u [i, j]

The Gubinelli germ and its defect

noncomputable def RoughPaths.gubinelliGerm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α (Fin d → E)) : ℝ → ℝ → E

The Gubinelli germ of a controlled integrand: the two-term local expansion of ∫_s^t Y dX.

Equations

• RoughPaths.gubinelliGerm Z s t = ∑ i : Fin d, X.coeff s t [i] • Z.Y s i + ∑ i : Fin d, ∑ j : Fin d, X.coeff s t [i, j] • Z.Yd s i j

theorem RoughPaths.gubinelliGerm_apply {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α (Fin d → E)) (s t : ℝ) : gubinelliGerm Z s t = ∑ i : Fin d, X.coeff s t [i] • Z.Y s i + ∑ i : Fin d, ∑ j : Fin d, X.coeff s t [i, j] • Z.Yd s i j

theorem RoughPaths.gubinelliGerm_defect_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α (Fin d → E)) (a b c : ℝ) : gubinelliGerm Z a c - gubinelliGerm Z a b - gubinelliGerm Z b c = ∑ j : Fin d, X.coeff b c [j] • (Z.Y a - Z.Y b + ∑ i : Fin d, X.coeff a b [i] • Z.Yd a i) j + ∑ i : Fin d, ∑ j : Fin d, X.coeff b c [i, j] • (Z.Yd a i j - Z.Yd b i j)

The algebraic defect identity: by Chen's relations the germ's defect is a remainder term paired with the first level plus a derivative increment paired with the second level.

theorem RoughPaths.enorm_apply_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {f : Fin d → E} (j : Fin d) : ‖f j‖ₑ ≤ ‖f‖ₑ

Coordinates of a Pi-valued vector are dominated by its sup norm.

theorem RoughPaths.gubinelliGerm_defect {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) (Z : ControlledPath X ω α (Fin d → E)) ⦃a b c : ℝ⦄ : a ≤ b → b ≤ c → ‖gubinelliGerm Z a c - gubinelliGerm Z a b - gubinelliGerm Z b c‖ₑ ≤ (↑d * ↑Z.Cy + ↑d ^ 2 * ↑Z.Cd) * ω.toFun a c ^ (3 * α)

The analytic defect bound: the germ's defect has order ω^{3α} with constant d·Cy + d²·Cd.

Existence, uniqueness, and controlledness of the rough integral

noncomputable def RoughPaths.roughConst {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α (Fin d → E)) : ENNReal

The defect constant of a controlled path.

Equations

• RoughPaths.roughConst Z = ↑d * ↑Z.Cy + ↑d ^ 2 * ↑Z.Cd

theorem RoughPaths.roughConst_ne_top {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α (Fin d → E)) : roughConst Z ≠ ⊤

theorem RoughPaths.exists_roughIntegral {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (hX : IsLevel2RoughPath X ω α) (Z : ControlledPath X ω α (Fin d → 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 - gubinelliGerm Z s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst Z * ω.toFun s t ^ (3 * α))) ∧ ∀ ⦃s t : ℝ⦄, s ≤ t → ∀ (ε : ENNReal) (mid : List ℝ), List.IsChain (fun (a b : ℝ) => a ≤ b ∧ (Control.constMul (roughConst Z ^ (3 * α)⁻¹) ω).toFun a b ≤ ε) (s :: (mid ++ [t])) → ‖I s t - Sewing.pairSum (gubinelliGerm Z) (s :: (mid ++ [t]))‖ₑ ≤ Sewing.sewingConst (3 * α) * (ε ^ (3 * α - 1) * (Control.constMul (roughConst Z ^ (3 * α)⁻¹) ω).toFun s t)

Existence of the rough integral (Gubinelli; FH Thm 4.10): an additive ∫ Y dX with the local estimate ‖∫_s^t Y dX - Σᵢ X¹ᵢ Yᵢ(s) - Σᵢⱼ X²ᵢⱼ Y'ᵢⱼ(s)‖ ≤ K·(d·Cy + d²·Cd)·ω^{3α}, approximating the compensated Riemann sums of every fine partition.

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

theorem RoughPaths.roughIntegral_sub_linear {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) (Z : ControlledPath X ω α (Fin d → E)) {I : ℝ → ℝ → E} (hgerm : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I s t - gubinelliGerm Z s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst Z * ω.toFun s t ^ (3 * α))) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖I s t - ∑ i : Fin d, X.coeff s t [i] • Z.Y s i‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst Z * ω.toFun s t ^ (3 * α)) + ↑d ^ 2 * ↑Z.Cb * ω.toFun s t ^ (2 * α)

The rough integral is controlled by X with Gubinelli derivative Y: subtracting only the first-level part leaves a remainder of order ω^{2α} plus the higher-order sewing error.