Explicit Picard parameters

The arithmetic side of RDE well-posedness: for every C³_b vector field there exist box constants, contraction weights, a window size δα and an offset constant Koff satisfying all the side conditions of the Picard theory — the box-closure inequalities of picardMap_inBox and the weighted contraction of the distance step, in its two-driver form with a (ρ₁+ρ₂)-linear offset (PicardParams.contr).

The construction is hierarchical: the structural (non-δα) couplings of the distance step form the acyclic chain a → b → e → c, so the weights are solved greedily (wc = 1, then we, wb, wa) and every residual coupling carries a factor δα, absorbed by choosing δα as the inverse of the total residual coefficient.

pT/pR… below are the coefficients of the distance-step slots collected as linear forms in the certificate tuple (a,b,c,e,ρ₁,ρ₂); the bridge to the literal slot formulas of solutionDriverStep and picardDist is pure ring and is performed in the well-posedness wrappers.

Collected coefficients of the distance step at box constants

noncomputable def RoughPaths.RDEVectorField3.pTa {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By : NNReal) : NNReal

a-coefficient of the germ-constant block mixedRoughConstN.

Equations

• V.pTa Bb Bd By = ↑d * (V.C3 * (↑d * Bb + By) ^ 2 + V.C2 * By) + ↑d ^ 2 * (V.C2 * Bd + V.C3 * Bb * (↑d * Bb + By))

noncomputable def RoughPaths.RDEVectorField3.pTb {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

b-coefficient of the germ-constant block.

Equations

• V.pTb Bb By = ↑d ^ 2 * (2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * V.C2 * (↑d * Bb + By) + ↑d ^ 3 * (V.C2 + V.C3 * (↑d * Bb + By)) * Bb

noncomputable def RoughPaths.RDEVectorField3.pTc {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) : NNReal

c-coefficient of the germ-constant block.

Equations

• V.pTc = ↑d ^ 2 * V.C1

noncomputable def RoughPaths.RDEVectorField3.pTe {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

e-coefficient of the germ-constant block.

Equations

• V.pTe Bb By = ↑d * (2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2) + ↑d * V.C1 + ↑d ^ 2 * (V.C2 + V.C3 * (↑d * Bb + By)) * Bb

noncomputable def RoughPaths.RDEVectorField3.pTr1 {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

ρ₁-coefficient of the germ-constant block.

Equations

• V.pTr1 Bb By = ↑d ^ 2 * Bb * (2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2) + ↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 3 * (V.C2 + V.C3 * (↑d * Bb + By)) * Bb ^ 2

noncomputable def RoughPaths.RDEVectorField3.pTr2 {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By : NNReal) : NNReal

ρ₂-coefficient of the germ-constant block.

Equations

• V.pTr2 Bb Bd By = ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))

noncomputable def RoughPaths.RDEVectorField3.pT {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By a b c e ρ₁ ρ₂ : NNReal) : NNReal

The germ-constant block mixedRoughConstN of the composed distance, collected as a linear form of the certificate tuple.

Equations

• V.pT Bb Bd By a b c e ρ₁ ρ₂ = V.pTa Bb Bd By * a + V.pTb Bb By * b + V.pTc * c + V.pTe Bb By * e + V.pTr1 Bb By * ρ₁ + V.pTr2 Bb Bd By * ρ₂

noncomputable def RoughPaths.RDEVectorField3.pRa {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

a-coefficient of the derivative-Hölder slot.

Equations

• V.pRa Bb By = ↑d * V.C2 * Bb + V.C3 * (↑d * Bb + By) ^ 2 + V.C2 * By

noncomputable def RoughPaths.RDEVectorField3.pRb {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

b-coefficient of the derivative-Hölder slot.

Equations

• V.pRb Bb By = ↑d * V.C1 + ↑d * (2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2)

noncomputable def RoughPaths.RDEVectorField3.pRe {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

e-coefficient of the derivative-Hölder slot.

Equations

• V.pRe Bb By = 2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2 + V.C1

noncomputable def RoughPaths.RDEVectorField3.pRr1 {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By : NNReal) : NNReal

ρ₁-coefficient of the derivative-Hölder slot.

Equations

• V.pRr1 Bb By = ↑d * V.C1 * Bb + ↑d * Bb * (2 * V.C2 * (↑d * Bb + By) + V.C3 * (↑d * Bb + By) ^ 2)

The distance-step slot formulas at box constants

noncomputable def RoughPaths.RDEVectorField3.pCMy {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By a b e ρ₁ : NNReal) : NNReal

The remainder slot of the composed mixed distance (compMixedDist) at box constants.

Equations

• V.pCMy Bb By a b e ρ₁ = V.C2 * (↑d * (b + ρ₁ * Bb) + e) * (↑d * Bb + By + (↑d * Bb + By)) + V.C3 * (a + (↑d * (b + ρ₁ * Bb) + e)) * (↑d * Bb + By) ^ 2 + V.C1 * e + V.C2 * a * By

noncomputable def RoughPaths.RDEVectorField3.pCMd {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By a b c e ρ₁ : NNReal) : NNReal

The derivative-Hölder slot of the composed mixed distance at box constants.

Equations

• V.pCMd Bb Bd By a b c e ρ₁ = V.C1 * c + V.C2 * a * Bd + V.C2 * (↑d * Bb + By) * b + (V.C2 * (↑d * (b + ρ₁ * Bb) + e) + V.C3 * (a + (↑d * (b + ρ₁ * Bb) + e)) * (↑d * Bb + By)) * Bb

noncomputable def RoughPaths.RDEVectorField3.pRCN {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By a b c e ρ₁ ρ₂ : NNReal) : NNReal

The mixed germ constant mixedRoughConstN of the composed distance at box constants.

Equations

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

noncomputable def RoughPaths.RDEVectorField3.pS0 {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By K δα a b c e ρ₁ ρ₂ : NNReal) : NNReal

The sup slot of the two-driver distance step at box constants.

Equations

• V.pS0 Bb Bd By K δα a b c e ρ₁ ρ₂ = (↑d * (V.C1 * a + ρ₁ * V.C0) + ↑d ^ 2 * (V.C1 * b + V.C2 * a * Bb + ρ₂ * (V.C1 * Bb)) + K * V.pRCN Bb Bd By a b c e ρ₁ ρ₂) * δα

noncomputable def RoughPaths.RDEVectorField3.pSc {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb By a b e ρ₁ : NNReal) : NNReal

The derivative-Hölder slot of the two-driver distance step at box constants.

Equations

• V.pSc Bb By a b e ρ₁ = ↑d * (V.C1 * b + V.C2 * a * Bb + ρ₁ * (V.C1 * Bb)) + V.pCMy Bb By a b e ρ₁

noncomputable def RoughPaths.RDEVectorField3.pSe {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (Bb Bd By K δα a b c e ρ₁ ρ₂ : NNReal) : NNReal

The remainder slot of the two-driver distance step at box constants.

Equations

• V.pSe Bb Bd By K δα a b c e ρ₁ ρ₂ = K * V.pRCN Bb Bd By a b c e ρ₁ ρ₂ * δα + ↑d ^ 2 * (V.C1 * b + V.C2 * a * Bb + ρ₂ * (V.C1 * Bb))

structure RoughPaths.RDEVectorField3.PicardParams {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (α : ℝ) : Type

A full set of Picard parameters for the vector field V at Hölder exponent α: box constants closed under the Picard map, hierarchical contraction weights, a window size and a driver-distance offset. The contr field is the weighted contraction of the (two-driver) distance step, stated against the collected slot coefficients; at ρ₁ = ρ₂ = 0 it is the contraction hypothesis of rde_exists and rde_unique, and in general it feeds itoLyons_dist_le.

• Bb : NNReal

  Box constant for the derivative sup.

• Bd : NNReal

  Box constant for the derivative Hölder norm.

• By : NNReal

  Box constant for the remainder.

• wa : NNReal

  Weight of the sup slot.

• wb : NNReal

  Weight of the derivative-sup slot.

• wc : NNReal

  Weight of the derivative-Hölder slot.

• we : NNReal

  Weight of the remainder slot.

• δα : NNReal

  The window size.

• Koff : NNReal

  The driver-distance offset.

• wa_pos : 0 < self.wa
• δα_pos : 0 < self.δα
• δα_le_one : self.δα ≤ 1
• box_b : V.C0 ≤ self.Bb
• box_d : V.C1 * (↑d * self.Bb + self.By) ≤ self.Bd
• box_y : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * self.By + V.C2 * (↑d * self.Bb + self.By) ^ 2) + ↑d ^ 2 * (V.C1 * self.Bd + V.C2 * self.Bb * (↑d * self.Bb + self.By))) * self.δα + ↑d ^ 2 * (V.C1 * self.Bb) ≤ self.By
• contr (a b c e ρ₁ ρ₂ : NNReal) : 2 * (self.wa * V.pS0 self.Bb self.Bd self.By (Sewing.sewingConst (3 * α)).toNNReal self.δα a b c e ρ₁ ρ₂ + self.wb * (V.C1 * a) + self.wc * V.pSc self.Bb self.By a b e ρ₁ + self.we * V.pSe self.Bb self.Bd self.By (Sewing.sewingConst (3 * α)).toNNReal self.δα a b c e ρ₁ ρ₂) ≤ self.wa * a + self.wb * b + self.wc * c + self.we * e + self.Koff * (ρ₁ + ρ₂)

theorem RoughPaths.RDEVectorField3.exists_picardParams {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField3 d E) (α : ℝ) : Nonempty (V.PicardParams α)

Existence of Picard parameters: every C³_b vector field admits box constants, weights, a window size and an offset satisfying all side conditions of the Picard theory.

Hypothesis-light well-posedness and Itô–Lyons continuity

theorem RoughPaths.RDEVectorField.IsRDESolution.weaken {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {V' : RDEVectorField d E} {hX : IsLevel2RoughPath X ω α} {hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1} {Z : ControlledPath X ω α E} {I : ℝ → ℝ → E} (hsol : V'.IsRDESolution hX hω1 Z I) {Bb Bd By : NNReal} (h1 : Z.Cb ≤ Bb) (h2 : Z.Cd ≤ Bd) (h3 : Z.Cy ≤ By) : V'.IsRDESolution hX hω1 (Z.weaken h1 h2 h3) I

An RDE solution stays a solution after weakening its certificates to box constants.

theorem RoughPaths.RDEVectorField3.rde_wellposed {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (V : RDEVectorField3 d E) (hX : IsLevel2RoughPath X ω α) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (y₀ : E) (P : V.PicardParams α) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑P.δα) : ∃ (Z : ControlledPath X ω α E) (I : ℝ → ℝ → E), V.IsRDESolution hX hω1 Z I ∧ Z.Y 0 = y₀ ∧ InBox P.Bb P.Bd P.By Z ∧ ∀ (Z' : ControlledPath X ω α E) (I' : ℝ → ℝ → E), V.IsRDESolution hX hω1 Z' I' → Z'.Y 0 = y₀ → InBox P.Bb P.Bd P.By Z' → ∀ (u : ℝ), Z'.Y u = Z.Y u

RDE well-posedness with constructed parameters (Friz–Hairer Thms 8.3/8.4, hypothesis-light form): on any window where ω^α ≤ P.δα and ω ≤ 1, the RDE dY = f(Y)·dX started at y₀ has a box-certified solution, unique among box-certified solutions. All arithmetic side conditions are discharged by P : PicardParams V α, which exists for every C³_b vector field (exists_picardParams).

theorem RoughPaths.RDEVectorField3.itoLyons_continuity {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₂ ω α ρ₁ ρ₂) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (P : V.PicardParams α) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑P.δα) {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) (h1 : Z₁.Cb = P.Bb) (h2 : Z₁.Cd = P.Bd) (h3 : Z₁.Cy = P.By) (h1' : Z₂.Cb = P.Bb) (h2' : Z₂.Cd = P.Bd) (h3' : Z₂.Cy = P.By) (u : ℝ) : dist (Z₁.Y u) (Z₂.Y u) ≤ ↑(P.Koff * (ρ₁ + ρ₂)) / ↑P.wa

Continuity of the Itô–Lyons map, packaged (universal-limit-type statement): box-exact solutions of the same RDE along two drivers at certified distance (ρ₁, ρ₂), from the same initial condition, are uniformly P.Koff·(ρ₁+ρ₂)/P.wa-close — a local Lipschitz estimate for the solution map in the rough path metric.

theorem RoughPaths.RDEVectorField3.itoLyons_continuity_edist {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ω : Control ℝ} {α : ℝ} [CompleteSpace E] (V : RDEVectorField3 d E) (A B : Level2RoughPath ω α d) {ρ : NNReal} (hAB : edist A B ≤ ↑ρ) (hω1 : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≤ 1) (hfine : Sewing.HasFinePartitions ω) (hωne : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (P : V.PicardParams α) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑P.δα) {Z₁ : ControlledPath A.X ω α E} {Z₂ : ControlledPath B.X ω α E} {I₁ I₂ : ℝ → ℝ → E} (hsol₁ : V.IsRDESolution ⋯ hω1 Z₁ I₁) (hsol₂ : V.IsRDESolution ⋯ hω1 Z₂ I₂) (h0 : Z₁.Y 0 = Z₂.Y 0) (h1 : Z₁.Cb = P.Bb) (h2 : Z₁.Cd = P.Bd) (h3 : Z₁.Cy = P.By) (h1' : Z₂.Cb = P.Bb) (h2' : Z₂.Cd = P.Bd) (h3' : Z₂.Cy = P.By) (u : ℝ) : dist (Z₁.Y u) (Z₂.Y u) ≤ ↑(P.Koff * (ρ + ρ)) / ↑P.wa

Continuity of the Itô–Lyons map in the rough path metric: for drivers at metric distance at most ρ in the space of level-2 rough paths, the corresponding solutions are uniformly 2·P.Koff·ρ/P.wa-close. The Itô–Lyons map is thus locally Lipschitz — in particular continuous — from the rough path topology to uniform convergence of solutions.