The Picard map for rough differential equations

The Picard map of dY = f(Y)·dX with initial condition y₀: a controlled path Z is sent to the path based at y₀ with increments the rough integral of the composed integrand f(Z), and Gubinelli derivative f(Z.Y). On a control window normalised by ω ≤ 1 and ω^α ≤ δα, the map preserves an explicit certificate box (for suitable box constants), the first step towards the fixed-point construction of solutions.

def RoughPaths.ControlledPath.roughConstN {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Z : ControlledPath X ω α W) : NNReal

The ℝ≥0-valued germ constant of a controlled path.

Equations

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

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

theorem RoughPaths.dist_le_coe_of_enorm_le {F : Type u_3} [NormedAddCommGroup F] {x y : F} {c : NNReal} (h : ‖y - x‖ₑ ≤ ↑c) : dist x y ≤ ↑c

Distance form of an extended-norm bound.

theorem RoughPaths.coe_le_geom_of_pow_mul_le {a ρ w : NNReal} {n : ℕ} (hw : 0 < w) (h : 2 ^ n * (w * a) ≤ ρ) : ↑a ≤ ↑ρ / ↑w * (1 / 2) ^ n

Geometric extraction: 2ⁿ·(w·a) ≤ ρ gives a ≤ (ρ/w)·(1/2)ⁿ.

Basing an additive increment family at an initial point

noncomputable def RoughPaths.basedPath {E : Type u_1} [NormedAddCommGroup E] (I : ℝ → ℝ → E) (y₀ : E) (t : ℝ) : E

The path based at y₀ with increments I.

Equations

• RoughPaths.basedPath I y₀ t = if 0 ≤ t then y₀ + I 0 t else y₀ - I t 0

theorem RoughPaths.basedPath_increment {E : Type u_1} [NormedAddCommGroup E] {I : ℝ → ℝ → E} (hadd : ∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I s u + I u t = I s t) (y₀ : E) ⦃s t : ℝ⦄ (hst : s ≤ t) : basedPath I y₀ t - basedPath I y₀ s = I s t

theorem RoughPaths.basedPath_zero {E : Type u_1} [NormedAddCommGroup E] {I : ℝ → ℝ → E} (hadd : ∀ ⦃s u t : ℝ⦄, s ≤ u → u ≤ t → I s u + I u t = I s t) (y₀ : E) : basedPath I y₀ 0 = y₀

The Picard map

noncomputable def RoughPaths.picardIntegral {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 ≠ ⊤) (Z : ControlledPath X ω α E) : ℝ → ℝ → E

The chosen rough integral of the composed integrand.

Equations

• RoughPaths.picardIntegral V hX hω1 hfine hωne Z = Classical.choose ⋯

theorem RoughPaths.picardIntegral_additive {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 ≠ ⊤) (Z : ControlledPath X ω α E) ⦃s u t : ℝ⦄ : s ≤ u → u ≤ t → picardIntegral V hX hω1 hfine hωne Z s u + picardIntegral V hX hω1 hfine hωne Z u t = picardIntegral V hX hω1 hfine hωne Z s t

theorem RoughPaths.picardIntegral_germ {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 ≠ ⊤) (Z : ControlledPath X ω α E) ⦃s t : ℝ⦄ : s ≤ t → ‖picardIntegral V hX hω1 hfine hωne Z 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 * α))

noncomputable def RoughPaths.picardMap {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 ≠ ⊤) {δα : NNReal} (y₀ : E) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (Z : ControlledPath X ω α E) : ControlledPath X ω α E

The Picard map: base point y₀, increments the rough integral of f(Z), Gubinelli derivative f(Z.Y), with explicit certificates.

Equations

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

@[simp]

theorem RoughPaths.picardMap_Yd {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 ≠ ⊤) {δα : NNReal} (y₀ : E) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (Z : ControlledPath X ω α E) (t : ℝ) (i : Fin d) : (picardMap V hX hω1 hfine hωne y₀ hδα Z).Yd t i = V.f i (Z.Y t)

theorem RoughPaths.picardMap_zero {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 ≠ ⊤) {δα : NNReal} (y₀ : E) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (Z : ControlledPath X ω α E) : (picardMap V hX hω1 hfine hωne y₀ hδα Z).Y 0 = y₀

Box invariance

def RoughPaths.InBox {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (Bb Bd By : NNReal) (Z : ControlledPath X ω α E) : Prop

Membership of the certificate box.

Equations

• RoughPaths.InBox Bb Bd By Z = (Z.Cb ≤ Bb ∧ Z.Cd ≤ Bd ∧ Z.Cy ≤ By)

theorem RoughPaths.picardMap_inBox {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 ≠ ⊤) {δα : NNReal} (y₀ : E) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) {Bb Bd By : NNReal} (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {Z : ControlledPath X ω α E} (hZ : InBox Bb Bd By Z) : InBox Bb Bd By (picardMap V hX hω1 hfine hωne y₀ hδα Z)

Box invariance of the Picard map: for box constants satisfying the three closure inequalities, the Picard map preserves the box.

The distance step

theorem RoughPaths.enorm_gubinelliGerm_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) (Z' : ControlledPath X ω α (Fin d → E)) {B0 : ENNReal} (hY : ∀ (s : ℝ), ‖Z'.Y s‖ₑ ≤ B0) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖gubinelliGerm Z' s t‖ₑ ≤ ↑d * B0 * ω.toFun s t ^ α + ↑d ^ 2 * ↑Z'.Cb * ω.toFun s t ^ (2 * α)

Pointwise bound for a Gubinelli germ from a sup bound on the path data.

theorem RoughPaths.integral_dist_bound {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 ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {Z₁ Z₂ : ControlledPath X ω α 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 (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.compControlledDist hX hω1 D).D0 + ↑d ^ 2 * (V.compControlledDist hX hω1 D).Db + (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.compControlledDist hX hω1 D).Dy + ↑d ^ 2 * (V.compControlledDist hX hω1 D).Dd)) * δα)

The difference of two additive families with sewing germ bounds for the composed integrands is bounded by the distance constants with the full window gain.

theorem RoughPaths.integral_sub_germ_folded {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 ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) {Z₁ Z₂ : ControlledPath X ω α 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 (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.compControlledDist hX hω1 D).toControlledPath s t‖ₑ ≤ ↑((Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.compControlledDist hX hω1 D).Dy + ↑d ^ 2 * (V.compControlledDist hX hω1 D).Dd) * δα) * ω.toFun s t ^ (2 * α)

The folded form of the integral-difference germ bound on the window.

noncomputable def RoughPaths.picardDist {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 ≠ ⊤) {δα : NNReal} (y₀ : E) (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {Z₁ Z₂ : ControlledPath X ω α E} (D : ControlledDist Z₁ Z₂) : ControlledDist (picardMap V hX hω1 hfine hωne y₀ hδα Z₁) (picardMap V hX hω1 hfine hωne y₀ hδα Z₂)

The distance step: certificates for the distance between two Picard iterates, linear in the input distance with an explicit window gain δα on the sup and remainder slots.

Equations

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

The distance step for a pair of solutions

noncomputable def RoughPaths.solutionDistStep {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 ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {Z₁ 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) (D : ControlledDist Z₁ Z₂) : ControlledDist Z₁ Z₂

The distance step for two solutions: solutions of the same RDE from the same initial condition satisfy the Picard distance-step inequalities directly, with their own increment families.

Equations

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

Uniqueness of solutions

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

Any two box-certified controlled paths with the same initial value admit a finite distance certificate on the window.

Equations

• RoughPaths.seedDist hX hω1 hδα h0 hZ₁ hZ₂ = { D0 := 2 * ((↑d * Bb + By) * δα), Db := 2 * Bb, Dd := 2 * Bd, Dy := 2 * By, bound_Y := ⋯, bound_Yd := ⋯, holder_Yd := ⋯, remainder := ⋯ }

theorem RoughPaths.rde_unique {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 ≠ ⊤) {δα : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) {Bb Bd By wa wb wc we : NNReal} (hwa : 0 < wa) {Z₁ 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 : ControlledDist Z₁ Z₂), 2 * (wa * (solutionDistStep V hX hω1 hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).D0 + wb * (solutionDistStep V hX hω1 hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Db + wc * (solutionDistStep V hX hω1 hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Dd + we * (solutionDistStep V hX hω1 hfine hωne hδα hδα1 hsol₁ hsol₂ h0 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) (u : ℝ) : Z₁.Y u = Z₂.Y u

Uniqueness of RDE solutions (Friz–Hairer Thm 8.4-type): two box-certified solutions of dY = f(Y)·dX from the same initial value coincide on the window, provided the distance step contracts a weighted combination of the distance certificates.

Weakening certificates

def RoughPaths.ControlledPath.weaken {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Bb Bd By : NNReal} (Z : ControlledPath X ω α W) (h1 : Z.Cb ≤ Bb) (h2 : Z.Cd ≤ Bd) (h3 : Z.Cy ≤ By) : ControlledPath X ω α W

Enlarge the certificates of a controlled path to given box constants.

Equations

• Z.weaken h1 h2 h3 = { Y := Z.Y, Yd := Z.Yd, Cb := Bb, Cd := Bd, Cy := By, bound_Yd := ⋯, holder_Yd := ⋯, remainder := ⋯ }

@[simp]

theorem RoughPaths.ControlledPath.weaken_Y {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Bb Bd By : NNReal} (Z : ControlledPath X ω α W) (h1 : Z.Cb ≤ Bb) (h2 : Z.Cd ≤ Bd) (h3 : Z.Cy ≤ By) : (Z.weaken h1 h2 h3).Y = Z.Y

@[simp]

theorem RoughPaths.ControlledPath.weaken_Yd {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Bb Bd By : NNReal} (Z : ControlledPath X ω α W) (h1 : Z.Cb ≤ Bb) (h2 : Z.Cd ≤ Bd) (h3 : Z.Cy ≤ By) : (Z.weaken h1 h2 h3).Yd = Z.Yd

def RoughPaths.ControlledDist.ofWeaken {d : ℕ} {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {Bb Bd By : NNReal} {Z₁ Z₂ : ControlledPath X ω α W} (D : ControlledDist Z₁ Z₂) (h1 : Z₁.Cb ≤ Bb) (h2 : Z₁.Cd ≤ Bd) (h3 : Z₁.Cy ≤ By) (h1' : Z₂.Cb ≤ Bb) (h2' : Z₂.Cd ≤ Bd) (h3' : Z₂.Cy ≤ By) : ControlledDist (Z₁.weaken h1 h2 h3) (Z₂.weaken h1' h2' h3')

Distance certificates transport across weakening (the paths are unchanged).

Equations

• D.ofWeaken h1 h2 h3 h1' h2' h3' = { D0 := D.D0, Db := D.Db, Dd := D.Dd, Dy := D.Dy, bound_Y := ⋯, bound_Yd := ⋯, holder_Yd := ⋯, remainder := ⋯ }

The Picard iteration

noncomputable def RoughPaths.picardSeq {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) : ℕ → { Z : ControlledPath X ω α E // Z.Cb = Bb ∧ Z.Cd = Bd ∧ Z.Cy = By ∧ Z.Y 0 = y₀ }

The Picard iterates: starting from the constant path, apply the Picard map and re-certify to the box at every step. All iterates carry literal box constants and start at y₀.

Equations

• One or more equations did not get rendered due to their size.
• RoughPaths.picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy 0 = ⟨(RoughPaths.ControlledPath.const X ω α y₀).weaken ⋯ ⋯ ⋯, ⋯⟩

noncomputable def RoughPaths.picardSeqDist {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) (n : ℕ) : ControlledDist ↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy (n + 1)) ↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy n)

Distance certificates between consecutive Picard iterates.

Equations

• One or more equations did not get rendered due to their size.
• RoughPaths.picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy 0 = RoughPaths.seedDist hX hω1 hδα ⋯ ⋯ ⋯

theorem RoughPaths.picardSeqDist_decay {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} (hcontr : ∀ (Z₁ Z₂ : ControlledPath X ω α E), Z₁.Cb = Bb → Z₁.Cd = Bd → Z₁.Cy = By → Z₂.Cb = Bb → Z₂.Cd = Bd → Z₂.Cy = By → ∀ (D : ControlledDist Z₁ Z₂), 2 * (wa * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).D0 + wb * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Db + wc * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dd + we * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) (n : ℕ) : 2 ^ n * (wa * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy n).D0 + wb * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy n).Db + wc * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy n).Dd + we * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy n).Dy) ≤ wa * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy 0).D0 + wb * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy 0).Db + wc * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy 0).Dd + we * (picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy 0).Dy

The weighted distance decays geometrically along the iteration.

noncomputable def RoughPaths.picardRho0 {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} : NNReal

Shorthand for the weighted seed distance.

Equations

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

theorem RoughPaths.picardSeq_dist_le {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} (hwa : 0 < wa) (hcontr : ∀ (Z₁ Z₂ : ControlledPath X ω α E), Z₁.Cb = Bb → Z₁.Cd = Bd → Z₁.Cy = By → Z₂.Cb = Bb → Z₂.Cd = Bd → Z₂.Cy = By → ∀ (D : ControlledDist Z₁ Z₂), 2 * (wa * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).D0 + wb * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Db + wc * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dd + we * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) (n : ℕ) (u : ℝ) : dist ((↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy n)).Y u) ((↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy (n + 1))).Y u) ≤ ↑(picardRho0 V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy) / ↑wa * (1 / 2) ^ n

Consecutive Picard iterates are geometrically close, pointwise.

theorem RoughPaths.picardSeq_cauchy {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} (hwa : 0 < wa) (hcontr : ∀ (Z₁ Z₂ : ControlledPath X ω α E), Z₁.Cb = Bb → Z₁.Cd = Bd → Z₁.Cy = By → Z₂.Cb = Bb → Z₂.Cd = Bd → Z₂.Cy = By → ∀ (D : ControlledDist Z₁ Z₂), 2 * (wa * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).D0 + wb * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Db + wc * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dd + we * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) (u : ℝ) : ∃ (L : E), Filter.Tendsto (fun (n : ℕ) => (↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy n)).Y u) Filter.atTop (nhds L)

The Picard iterates converge pointwise: the limit path.

theorem RoughPaths.picardIntegral_dist_le {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) (n : ℕ) ⦃s t : ℝ⦄ : s ≤ t → ‖picardIntegral V hX hω1 hfine hωne (↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy (n + 1))) s t - picardIntegral V hX hω1 hfine hωne (↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy n)) s t‖ₑ ≤ ↑(picardSeqDist V hX hω1 hfine hωne y₀ hδα hδα1 hBb hBd hBy (n + 1)).D0

Consecutive Picard integrals are close, with the next distance constant.

theorem RoughPaths.picardIntegral_cauchy {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} (hwa : 0 < wa) (hcontr : ∀ (Z₁ Z₂ : ControlledPath X ω α E), Z₁.Cb = Bb → Z₁.Cd = Bd → Z₁.Cy = By → Z₂.Cb = Bb → Z₂.Cd = Bd → Z₂.Cy = By → ∀ (D : ControlledDist Z₁ Z₂), 2 * (wa * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).D0 + wb * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Db + wc * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dd + we * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) ⦃s t : ℝ⦄ (hst : s ≤ t) : ∃ (L : E), Filter.Tendsto (fun (n : ℕ) => picardIntegral V hX hω1 hfine hωne (↑(picardSeq V hX hω1 hfine hωne y₀ hδα hBb hBd hBy n)) s t) Filter.atTop (nhds L)

The Picard integrals converge pointwise on ordered pairs.

theorem RoughPaths.rde_exists {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 ≠ ⊤) {δα : NNReal} (y₀ : E) {Bb Bd By : NNReal} (hδα : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ^ α ≤ ↑δα) (hδα1 : δα ≤ 1) (hBb : V.C0 ≤ Bb) (hBd : V.C1 * (↑d * Bb + By) ≤ Bd) (hBy : (Sewing.sewingConst (3 * α)).toNNReal * (↑d * (V.C1 * By + V.C2 * (↑d * Bb + By) ^ 2) + ↑d ^ 2 * (V.C1 * Bd + V.C2 * Bb * (↑d * Bb + By))) * δα + ↑d ^ 2 * (V.C1 * Bb) ≤ By) {wa wb wc we : NNReal} (hwa : 0 < wa) (hcontr : ∀ (Z₁ Z₂ : ControlledPath X ω α E), Z₁.Cb = Bb → Z₁.Cd = Bd → Z₁.Cy = By → Z₂.Cb = Bb → Z₂.Cd = Bd → Z₂.Cy = By → ∀ (D : ControlledDist Z₁ Z₂), 2 * (wa * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).D0 + wb * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Db + wc * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dd + we * (picardDist V hX hω1 hfine hωne y₀ hδα hδα1 D).Dy) ≤ wa * D.D0 + wb * D.Db + wc * D.Dd + we * D.Dy) : ∃ (Z : ControlledPath X ω α E) (I : ℝ → ℝ → E), V.IsRDESolution hX hω1 Z I ∧ Z.Y 0 = y₀ ∧ InBox Bb Bd By Z

Existence of RDE solutions (Friz–Hairer Thm 8.3-type): under the box-closure and weighted-contraction window conditions, the Picard iterates converge to a box-certified solution of dY = f(Y)·dX started at y₀.