Continuity of the Itô–Lyons map

The quantitative core of the universal limit theorem (Friz–Hairer Thm 8.5): two box-certified solutions of dY = f(Y)·dX₁ and dY = f(Y)·dX₂ from the same initial condition, driven by rough paths at certified distance (ρ₁, ρ₂), stay uniformly within Coff/wa of each other — where Coff is the affine offset of the two-driver distance step (solutionDriverStep), which vanishes with (ρ₁, ρ₂) → 0.

The mechanism is an affine fixed-point iteration: the mixed distance step contracts the weighted certificate up to the ρ-offset, so iterating from the seed certificate gives ρ_w(n) ≤ (1/2)ⁿ·ρ_w(0) + Coff and the pointwise distance of the two solutions is dominated by every ρ_w(n)/wa.

theorem RoughPaths.RDEVectorField3.itoLyons_dist_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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₂ ω α ρ₁ ρ₂) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {Bb Bd By wa wb wc we Coff : NNReal} (hwa : 0 < wa) {Z₁ : ControlledPath X₁ ω α E} {Z₂ : ControlledPath X₂ ω α E} {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) (hZ₁ : InBox Bb Bd By Z₁) (hZ₂ : InBox Bb Bd By Z₂) (hcontr : ∀ (D : MixedDist Z₁ Z₂), 2 * (wa * (V.solutionDriverStep hX₁ hX₂ hω1 hXd hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).D0 + wb * (V.solutionDriverStep hX₁ hX₂ hω1 hXd hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Db + wc * (V.solutionDriverStep hX₁ hX₂ hω1 hXd hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Dd + we * (V.solutionDriverStep hX₁ hX₂ hω1 hXd hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy + Coff) (u : ℝ) : dist (Z₁.Y u) (Z₂.Y u) ≤ ↑Coff / ↑wa

Continuity of the Itô–Lyons map (Friz–Hairer Thm 8.5-type, quantitative form): two box-certified solutions along drivers at certified distance (ρ₁, ρ₂) from the same initial condition satisfy dist (Y¹_u, Y²_u) ≤ Coff / wa for every time u, where Coff is any affine offset for the weighted two-driver distance step. Since the step slots are polynomial in (ρ₁, ρ₂) with no constant term beyond the one-driver formulas, Coff can be taken linear in (ρ₁, ρ₂); the solution therefore depends continuously — indeed Lipschitz-continuously — on the driving rough path.