Stability of the rough integral and RDE solutions in the driver

The two-driver stability calculus behind the continuity of the Itô–Lyons map (Friz–Hairer §8.3): controlled paths over different level-2 rough paths X₁, X₂ at certified distance (ρ₁, ρ₂) (RoughPathDist) are compared through MixedDist certificates, whose remainder slot measures the difference of the two own-driver remainders. Every one-driver estimate of RDE/Stability and RDE/Picard has a two-driver analogue here, with the same certificate formulas plus explicit ρ-offsets:

• MixedDist.increment_sub_le — increment of the difference path;
• mixed_germ_defect — the defect of the difference of germs is of order ω^{3α} with constant d(Dy + ρ₁Cy) + d²(Dd + ρ₂Cd);
• mixedIntegral_sub — sewing: the difference of the two rough integrals is within K·(mixed constant)·ω^{3α} of the germ difference;
• mixed_integral_dist_bound / mixed_integral_sub_germ_folded — the window-gain forms feeding the distance-step slots.

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

Certified distance data between controlled paths over different drivers. The remainder slot bounds the difference of the two own-driver remainders (Friz–Hairer's "distance with different rough paths").

• 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

  Bound for the difference of the own-driver remainders.

• 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 s - ∑ i : Fin d, X₁.coeff s t [i] • Z₁.Yd s i - (Z₂.Y t - Z₂.Y s - ∑ i : Fin d, X₂.coeff s t [i] • Z₂.Yd s i)‖ₑ ≤ ↑self.Dy * ω.toFun s t ^ (2 * α)

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

The increment of the difference of two controlled paths over different drivers: the one-driver bound plus the offset d·ρ₁·Cb₁.

The difference of two Gubinelli germs

theorem RoughPaths.enorm_gubinelliGerm_sub_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} {Z₁' : ControlledPath X₁ ω α (Fin d → E)} {Z₂' : ControlledPath X₂ ω α (Fin d → E)} (hX₂ : IsLevel2RoughPath X₂ ω α) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) (DW : MixedDist Z₁' Z₂') {B₁ : NNReal} (hB₁ : ∀ (s : ℝ), ‖Z₁'.Y s‖ₑ ≤ ↑B₁) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖gubinelliGerm Z₁' s t - gubinelliGerm Z₂' s t‖ₑ ≤ ↑d * (↑DW.D0 + ↑ρ₁ * ↑B₁) * ω.toFun s t ^ α + ↑d ^ 2 * (↑DW.Db + ↑ρ₂ * ↑Z₁'.Cb) * ω.toFun s t ^ (2 * α)

Sup bound for the difference of two Gubinelli germs over different drivers, from a sup bound B₁ on the first integrand.

noncomputable def RoughPaths.mixedRoughConstN {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Z₂' : ControlledPath X₂ ω α (Fin d → E)} (Z₁' : ControlledPath X₁ ω α (Fin d → E)) (DW : MixedDist Z₁' Z₂') (ρ₁ ρ₂ : NNReal) : NNReal

The mixed defect constant: the one-driver d·Dy + d²·Dd with the driver-distance offsets d·ρ₁·Cy₁ + d²·ρ₂·Cd₁.

Equations

• RoughPaths.mixedRoughConstN Z₁' DW ρ₁ ρ₂ = ↑d * (DW.Dy + ρ₁ * Z₁'.Cy) + ↑d ^ 2 * (DW.Dd + ρ₂ * Z₁'.Cd)

theorem RoughPaths.mixed_germ_defect {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} {Z₁' : ControlledPath X₁ ω α (Fin d → E)} {Z₂' : ControlledPath X₂ ω α (Fin d → E)} (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) (DW : MixedDist Z₁' Z₂') ⦃a b c : ℝ⦄ : a ≤ b → b ≤ c → ‖gubinelliGerm Z₁' a c - gubinelliGerm Z₂' a c - (gubinelliGerm Z₁' a b - gubinelliGerm Z₂' a b) - (gubinelliGerm Z₁' b c - gubinelliGerm Z₂' b c)‖ₑ ≤ ↑(mixedRoughConstN Z₁' DW ρ₁ ρ₂) * ω.toFun a c ^ (3 * α)

The mixed defect bound: the defect of the difference of the two Gubinelli germs is of order ω^{3α} with the mixed constant. This is the two-driver core of the Itô–Lyons continuity.

theorem RoughPaths.mixedIntegral_sub {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} {Z₁' : ControlledPath X₁ ω α (Fin d → E)} {Z₂' : ControlledPath X₂ ω α (Fin d → E)} [CompleteSpace E] (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (DW : MixedDist 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 Z₁' s t - gubinelliGerm Z₂' s t)‖ₑ ≤ Sewing.sewingConst (3 * α) * (↑(mixedRoughConstN Z₁' DW ρ₁ ρ₂) * ω.toFun s t ^ (3 * α))

Two-driver stability of the rough integral: the difference of two rough integrals over different drivers is within the mixed germ constant of the difference of the germs.

Two-driver stability of composition

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

Two-driver stability of composition (Friz–Hairer Lemma 7.5-type): mixed distance certificates between f(Y¹) (over X₁) and f(Y²) (over X₂), linear in the mixed certificates of Y¹, Y² with the driver-distance offset entering only through the increment constant d·(Db + ρ₁·Cb₁) + Dy.

Equations

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

Window-gain bounds for the mixed integral difference

theorem RoughPaths.RDEVectorField3.comp_bound_Y {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 : ControlledPath X₁ ω α E) (s : ℝ) : ‖(V.compControlled hX₁ hω1 Z).Y s‖ₑ ≤ ↑V.C0

The composed integrand is uniformly bounded by C₀.

theorem RoughPaths.RDEVectorField3.mixed_integral_dist_bound {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} [CompleteSpace E] (V : RDEVectorField3 d E) (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) {Z₁ : ControlledPath X₁ ω α E} {Z₂ : ControlledPath X₂ ω α E} (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (D : MixedDist 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 (V.compControlled hX₁ hω1 Z₁) s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst (V.compControlled hX₁ hω1 Z₁) * ω.toFun s t ^ (3 * α))) (hgerm₂ : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I₂ s t - gubinelliGerm (V.compControlled hX₂ hω1 Z₂) s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst (V.compControlled hX₂ hω1 Z₂) * ω.toFun s t ^ (3 * α))) ⦃s t : ℝ⦄ : s ≤ t → ‖I₁ s t - I₂ s t‖ₑ ≤ ↑((↑d * ((V.compMixedDist hX₁ hX₂ hω1 hXd D).D0 + ρ₁ * V.C0) + ↑d ^ 2 * ((V.compMixedDist hX₁ hX₂ hω1 hXd D).Db + ρ₂ * (V.compControlled hX₁ hω1 Z₁).Cb) + (Sewing.sewingConst (3 * α)).toNNReal * mixedRoughConstN (V.compControlled hX₁ hω1 Z₁) (V.compMixedDist hX₁ hX₂ hω1 hXd D) ρ₁ ρ₂) * δα)

Mixed analogue of integral_dist_bound: the difference of the two rough integrals over different drivers gains the full window factor.

theorem RoughPaths.RDEVectorField3.mixed_integral_sub_germ_folded {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} [CompleteSpace E] (V : RDEVectorField3 d E) (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) {Z₁ : ControlledPath X₁ ω α E} {Z₂ : ControlledPath X₂ ω α E} (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (D : MixedDist 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 (V.compControlled hX₁ hω1 Z₁) s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst (V.compControlled hX₁ hω1 Z₁) * ω.toFun s t ^ (3 * α))) (hgerm₂ : ∀ ⦃s t : ℝ⦄, s ≤ t → ‖I₂ s t - gubinelliGerm (V.compControlled hX₂ hω1 Z₂) s t‖ₑ ≤ Sewing.sewingConst (3 * α) * (roughConst (V.compControlled hX₂ hω1 Z₂) * ω.toFun s t ^ (3 * α))) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖I₁ s t - I₂ s t - (gubinelliGerm (V.compControlled hX₁ hω1 Z₁) s t - gubinelliGerm (V.compControlled hX₂ hω1 Z₂) s t)‖ₑ ≤ ↑((Sewing.sewingConst (3 * α)).toNNReal * mixedRoughConstN (V.compControlled hX₁ hω1 Z₁) (V.compMixedDist hX₁ hX₂ hω1 hXd D) ρ₁ ρ₂ * δα) * ω.toFun s t ^ (2 * α)

Mixed analogue of integral_sub_germ_folded.

The distance step for solutions along two drivers

noncomputable def RoughPaths.RDEVectorField3.solutionDriverStep {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {ρ₁ ρ₂ : NNReal} [CompleteSpace E] (V : RDEVectorField3 d E) (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) (hXd : RoughPathDist X₁ X₂ ω α ρ₁ ρ₂) {Z₁ : ControlledPath X₁ ω α E} {Z₂ : ControlledPath X₂ ω α E} (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {I₁ I₂ : ℝ → ℝ → E} (hsol₁ : V.IsRDESolution hX₁ hω1 Z₁ I₁) (hsol₂ : V.IsRDESolution hX₂ hω1 Z₂ I₂) (h0 : Z₁.Y 0 = Z₂.Y 0) (D : MixedDist Z₁ Z₂) : MixedDist Z₁ Z₂

The two-driver distance step: solutions of dY = f(Y)·dX₁ and dY = f(Y)·dX₂ from the same initial condition satisfy the mixed distance-step inequalities — the one-driver step formulas plus explicit (ρ₁, ρ₂)-offsets.

Equations

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

noncomputable def RoughPaths.RDEVectorField3.mixedSeedDist {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X₁ X₂ : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX₁ : IsLevel2RoughPath X₁ ω α) (hX₂ : IsLevel2RoughPath X₂ ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) {Z₁ : ControlledPath X₁ ω α E} {Z₂ : ControlledPath X₂ ω α E} {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) {Bb Bd By : NNReal} (h0 : Z₁.Y 0 = Z₂.Y 0) (hZ₁ : InBox Bb Bd By Z₁) (hZ₂ : InBox Bb Bd By Z₂) : MixedDist Z₁ Z₂

Any two box-certified controlled paths over different drivers with the same initial value admit a finite mixed distance certificate.

Equations

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