Composition of controlled paths with vector fields

Friz–Hairer Lemma 7.3, the key step towards RDE well-posedness: if Y is controlled by X with Gubinelli derivative Y', and V = (f, Df) is a vector field with bounded, Lipschitz derivative, then t ↦ f(Y_t) is again controlled by X, with Gubinelli derivative Df(Y_t)∘Y'_t and fully explicit certificates. The remainder analysis combines the first-order Taylor bound ‖f(z) - f(y) - Df(y)(z-y)‖ ≤ C₂‖z-y‖² (from the mean value inequality applied to w ↦ f(w) - Df(y)w) with the controlled remainder of Y pushed through Df.

All estimates are stated on a control window ω ≤ 1, the normalisation under which the Picard iteration is run.

Window arithmetic for control powers

theorem RoughPaths.rpow_two_mul_eq {α : ℝ} (hα : 0 ≤ α) (x : ENNReal) : x ^ (2 * α) = x ^ α * x ^ α

theorem RoughPaths.rpow_three_mul_eq {α : ℝ} (hα : 0 ≤ α) (x : ENNReal) : x ^ (3 * α) = x ^ α * x ^ (2 * α)

theorem RoughPaths.rpow_pow_two {α : ℝ} (x : ENNReal) : (x ^ α) ^ 2 = x ^ (2 * α)

theorem RoughPaths.rpow_three_mul_le_mul {α : ℝ} {x : ENNReal} {δα : NNReal} (hα : 0 ≤ α) (hδ : x ^ α ≤ ↑δα) : x ^ (3 * α) ≤ ↑δα * x ^ (2 * α)

theorem RoughPaths.rpow_two_mul_le_coe {α : ℝ} {x : ENNReal} {δα : NNReal} (hα : 0 ≤ α) (hδ : x ^ α ≤ ↑δα) (hδ1 : δα ≤ 1) : x ^ (2 * α) ≤ ↑δα

theorem RoughPaths.rpow_three_mul_le_coe {α : ℝ} {x : ENNReal} {δα : NNReal} (hα : 0 ≤ α) (hδ : x ^ α ≤ ↑δα) (hδ1 : δα ≤ 1) : x ^ (3 * α) ≤ ↑δα

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

A vector field driving an RDE: components f i : E → E with globally bounded, globally Lipschitz derivatives, all constants explicit. Any C²_b vector field yields such data.

• f : Fin d → E → E

  The components of the vector field.

• deriv : Fin d → E → E →L[ℝ] E

  The derivative of each component.

• C0 : NNReal

  Sup bound for the components.

• C1 : NNReal

  Sup bound for the derivatives.

• C2 : NNReal

  Lipschitz constant of the derivatives.

• 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‖

Extended-norm utilities

theorem RoughPaths.RDEVectorField.enorm_le_coe {F : Type u_2} [NormedAddCommGroup F] {x : F} {c : NNReal} (h : ‖x‖ ≤ ↑c) : ‖x‖ₑ ≤ ↑c

theorem RoughPaths.RDEVectorField.enorm_clm_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) (x : E) : ‖L x‖ₑ ≤ ‖L‖ₑ * ‖x‖ₑ

theorem RoughPaths.RDEVectorField.enorm_lipschitz {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField d E) (i : Fin d) (y z : E) : ‖V.deriv i y - V.deriv i z‖ₑ ≤ ↑V.C2 * ‖y - z‖ₑ

theorem RoughPaths.RDEVectorField.pi_enorm_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {g : Fin d → E} {C : ENNReal} (h : ∀ (i : Fin d), ‖g i‖ₑ ≤ C) : ‖g‖ₑ ≤ C

Coordinatewise extended-norm bounds give a Pi sup-norm bound.

The first-order Taylor bound

theorem RoughPaths.RDEVectorField.taylor_norm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField d E) (i : Fin d) (y z : E) : ‖V.f i z - V.f i y - (V.deriv i y) (z - y)‖ ≤ ↑V.C2 * ‖z - y‖ ^ 2

First-order Taylor estimate for a vector field with Lipschitz derivative: ‖f(z) - f(y) - Df(y)(z-y)‖ ≤ C₂·‖z-y‖².

theorem RoughPaths.RDEVectorField.taylor_enorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (V : RDEVectorField d E) (i : Fin d) (y z : E) : ‖V.f i z - V.f i y - (V.deriv i y) (z - y)‖ₑ ≤ ↑V.C2 * ‖z - y‖ₑ ^ 2

The Taylor estimate in extended norms.

Composition (Friz–Hairer Lemma 7.3)

theorem RoughPaths.RDEVectorField.increment_le {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) (Z : ControlledPath X ω α E) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖Z.Y t - Z.Y s‖ₑ ≤ (↑d * ↑Z.Cb + ↑Z.Cy) * ω.toFun s t ^ α

The increment of a controlled path on a unit control window is of order ω^α with constant d·Cb + Cy.

noncomputable def RoughPaths.RDEVectorField.compControlled {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) : ControlledPath X ω α (Fin d → E)

Composition of a controlled path with a vector field (FH Lemma 7.3): t ↦ (f i (Y t))_i is controlled by X with Gubinelli derivative (Df i (Y t) (Y'_j t))_{ij} and explicit certificates.

Equations

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

@[simp]

theorem RoughPaths.RDEVectorField.compControlled_Y {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) (t : ℝ) (i : Fin d) : (V.compControlled hX hω1 Z).Y t i = V.f i (Z.Y t)

@[simp]

theorem RoughPaths.RDEVectorField.compControlled_Yd {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) (t : ℝ) (j i : Fin d) : (V.compControlled hX hω1 Z).Yd t j i = (V.deriv i (Z.Y t)) (Z.Yd t j)