Stability of the rough integral in the integrand

Certified distances between controlled paths: a ControlledDist Z₁ Z₂ carries sup, derivative-sup, derivative-Hölder and remainder bounds for the difference Z₁ - Z₂, making the difference itself a controlled path. The Gubinelli germ is linear in the controlled-path data, so by the uniqueness half of the sewing lemma the difference of two rough integrals is the rough integral of the difference — with the small germ constant roughConst of the difference, the key input to the Picard contraction.

structure RoughPaths.ControlledDist {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z₁ Z₂ : ControlledPath X ω α W) : Type

Certified distance data between two controlled paths: quantitative bounds on the difference path, its Gubinelli derivative, and their regularity.

• D0 : NNReal

  Sup bound for the difference of paths.

• Db : NNReal

  Sup bound for the difference of derivatives.

• Dd : NNReal

  Hölder constant of the difference of derivatives.

• Dy : NNReal

  Remainder constant of the difference.

• bound_Y (s : ℝ) : ‖Z₁.Y s - Z₂.Y s‖ₑ ≤ ↑self.D0
• bound_Yd (s : ℝ) (i : Fin d) : ‖Z₁.Yd s i - Z₂.Yd s i‖ₑ ≤ ↑self.Db
• holder_Yd ⦃s t : ℝ⦄ : s ≤ t → ∀ (i : Fin d), ‖Z₁.Yd t i - Z₂.Yd t i - (Z₁.Yd s i - Z₂.Yd s i)‖ₑ ≤ ↑self.Dd * ω.toFun s t ^ α
• remainder ⦃s t : ℝ⦄ : s ≤ t → ‖Z₁.Y t - Z₂.Y t - (Z₁.Y s - Z₂.Y s) - ∑ i : Fin d, X.coeff s t [i] • (Z₁.Yd s i - Z₂.Yd s i)‖ₑ ≤ ↑self.Dy * ω.toFun s t ^ (2 * α)

def RoughPaths.ControlledDist.toControlledPath {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) : ControlledPath X ω α W

The difference of two controlled paths, as a controlled path with the distance certificates.

Equations

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

@[simp]

theorem RoughPaths.ControlledDist.toControlledPath_Y {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) (t : ℝ) : D.toControlledPath.Y t = Z₁.Y t - Z₂.Y t

@[simp]

theorem RoughPaths.ControlledDist.toControlledPath_Yd {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) (t : ℝ) (i : Fin d) : D.toControlledPath.Yd t i = Z₁.Yd t i - Z₂.Yd t i

@[simp]

theorem RoughPaths.ControlledDist.toControlledPath_Cb {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) : D.toControlledPath.Cb = D.Db

@[simp]

theorem RoughPaths.ControlledDist.toControlledPath_Cd {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) : D.toControlledPath.Cd = D.Dd

@[simp]

theorem RoughPaths.ControlledDist.toControlledPath_Cy {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) : D.toControlledPath.Cy = D.Dy

theorem RoughPaths.gubinelliGerm_sub {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₁ Z₂ : ControlledPath X ω α (Fin d → E)} (D : ControlledDist Z₁ Z₂) (s t : ℝ) : gubinelliGerm Z₁ s t - gubinelliGerm Z₂ s t = gubinelliGerm D.toControlledPath s t

Linearity of the Gubinelli germ in the controlled-path data.

theorem RoughPaths.ControlledDist.increment_sub_le {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖Z₁.Y t - Z₁.Y s - (Z₂.Y t - Z₂.Y s)‖ₑ ≤ (↑d * ↑D.Db + ↑D.Dy) * ω.toFun s t ^ α

The increment of the difference of two controlled paths.

theorem RoughPaths.roughIntegral_sub {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (hX : IsLevel2RoughPath X ω α) (hfine : Sewing.HasFinePartitions ω) (hω : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {Z₁ Z₂ : ControlledPath X ω α (Fin d → E)} (D : ControlledDist Z₁ Z₂) {I₁ I₂ : ℝ → ℝ → E} (hadd₁ : ∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I₁ s u + I₁ u t = I₁ s t) (hadd₂ : ∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I₂ s u + I₂ u t = I₂ s t) (hgerm₁ : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I₁ s t - gubinelliGerm Z₁ s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst Z₁ * ω.toFun s t ^ (3 * α))) (hgerm₂ : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I₂ s t - gubinelliGerm Z₂ s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst Z₂ * ω.toFun s t ^ (3 * α))) ⦃s t : ℝ⦄ : s ≤ t → ‖I₁ s t - I₂ s t - gubinelliGerm D.toControlledPath s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst D.toControlledPath * ω.toFun s t ^ (3 * α))

Stability of the rough integral in the integrand: the difference of two rough integrals is controlled by the distance germ constant of the integrands — not merely by the sum of their individual constants.

Two-path estimates for a vector field with Lipschitz second

derivative

structure RoughPaths.RDEVectorField3 (d : ℕ) (E : Type u_3) [NormedAddCommGroup E] [NormedSpace ℝ E] extends RoughPaths.RDEVectorField d E : Type u_3

A vector field with second-derivative data: the base RDEVectorField together with a bounded, Lipschitz second derivative (a C³_b-type assumption, needed for the Lipschitz dependence of the composition on the controlled path, as in Friz–Hairer Thm 8.4).

• f : Fin d → E → E
• deriv : Fin d → E → E →L[ℝ] E
• C0 : NNReal
• C1 : NNReal
• C2 : NNReal
• hasFDeriv (i : Fin d) (y : E) : HasFDerivAt (self.f i) (self.deriv i y) y
• bound_f (i : Fin d) (y : E) : ‖self.f i y‖ ≤ ↑self.C0
• bound_deriv (i : Fin d) (y : E) : ‖self.deriv i y‖ ≤ ↑self.C1
• lipschitz_deriv (i : Fin d) (y z : E) : ‖self.deriv i y - self.deriv i z‖ ≤ ↑self.C2 * ‖y - z‖
• deriv2 : Fin d → E → E →L[ℝ] E →L[ℝ] E

  The second derivative of each component.

• C3 : NNReal

  Lipschitz constant of the second derivatives.

• hasFDeriv2 (i : Fin d) (y : E) : HasFDerivAt (self.deriv i) (self.deriv2 i y) y
• bound_deriv2 (i : Fin d) (y : E) : ‖self.deriv2 i y‖ ≤ ↑self.C2
• lipschitz_deriv2 (i : Fin d) (y z : E) : ‖self.deriv2 i y - self.deriv2 i z‖ ≤ ↑self.C3 * ‖y - z‖

theorem RoughPaths.RDEVectorField3.f_lipschitz {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (y z : E) : ‖V.f i z - V.f i y‖ ≤ ↑V.C1 * ‖z - y‖

Components of the vector field are C₁-Lipschitz.

theorem RoughPaths.RDEVectorField3.deriv_double_diff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (y₁ y₂ v₁ v₂ : E) : ‖V.deriv i (y₁ + v₁) - V.deriv i y₁ - (V.deriv i (y₂ + v₂) - V.deriv i y₂)‖ ≤ ↑V.C2 * ‖v₁ - v₂‖ + ↑V.C3 * (‖y₁ - y₂‖ + ‖v₁ - v₂‖) * ‖v₂‖

Second-order double difference: derivative increments along two segments differ by at most C₂‖v₁-v₂‖ + C₃(‖y₁-y₂‖+‖v₁-v₂‖)‖v₂‖.

theorem RoughPaths.RDEVectorField3.taylor_diff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (y₁ y₂ Δ₁ Δ₂ : E) : ‖V.f i (y₁ + Δ₁) - V.f i y₁ - (V.deriv i y₁) Δ₁ - (V.f i (y₂ + Δ₂) - V.f i y₂ - (V.deriv i y₂) Δ₂)‖ ≤ ↑V.C2 * ‖Δ₁ - Δ₂‖ * (‖Δ₁‖ + ‖Δ₂‖) + ↑V.C3 * (‖y₁ - y₂‖ + ‖Δ₁ - Δ₂‖) * ‖Δ₂‖ ^ 2

Two-path Taylor difference: the Taylor remainders of f along two base points and increments differ by at most C₂‖Δ₁-Δ₂‖(‖Δ₁‖+‖Δ₂‖) + C₃(‖y₁-y₂‖+‖Δ₁-Δ₂‖)‖Δ₂‖².

Extended-norm endpoint forms

theorem RoughPaths.RDEVectorField3.enorm_f_lipschitz {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (a b : E) : ‖V.f i a - V.f i b‖ₑ ≤ ↑V.C1 * ‖a - b‖ₑ

theorem RoughPaths.RDEVectorField3.enorm_deriv_double_diff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (a b c e : E) : ‖V.deriv i a - V.deriv i b - (V.deriv i c - V.deriv i e)‖ₑ ≤ ↑V.C2 * ‖a - b - (c - e)‖ₑ + ↑V.C3 * (‖b - e‖ₑ + ‖a - b - (c - e)‖ₑ) * ‖c - e‖ₑ

The second-order double difference in extended norms, endpoint form.

theorem RoughPaths.RDEVectorField3.enorm_taylor_diff {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (i : Fin d) (a b c e : E) : ‖V.f i a - V.f i b - (V.deriv i b) (a - b) - (V.f i c - V.f i e - (V.deriv i e) (c - e))‖ₑ ≤ ↑V.C2 * ‖a - b - (c - e)‖ₑ * (‖a - b‖ₑ + ‖c - e‖ₑ) + ↑V.C3 * (‖b - e‖ₑ + ‖a - b - (c - e)‖ₑ) * ‖c - e‖ₑ ^ 2

The two-path Taylor difference in extended norms, endpoint form.

Two-path stability of composition (Friz–Hairer Lemma 7.4)

noncomputable def RoughPaths.RDEVectorField3.compControlledDist {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) {Z₁ Z₂ : ControlledPath X ω α E} (D : ControlledDist Z₁ Z₂) : ControlledDist (V.compControlled hX hω1 Z₁) (V.compControlled hX hω1 Z₂)

Two-path stability of composition: distance certificates between f(Y¹) and f(Y²) linear in the distance certificates of Y¹, Y².

Equations

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