Level-2 rough paths and controlled paths

Analytic regularity for a d-dimensional rough path with respect to a control ω: the first-level coordinates are bounded by ω^α and the second-level ones by ω^{2α}, with 1/3 < α ≤ 1/2. A path Y is controlled by such a rough path (Gubinelli) when it admits a derivative Y' along the first level with remainder of order ω^{2α}. Certificates (the constants) are carried as data so that all downstream estimates are fully quantitative.

structure RoughPaths.IsLevel2RoughPath {d : ℕ} (X : AlgebraicRoughPath ℝ (Fin d) ℝ) (ω : Control ℝ) (α : ℝ) : Prop

Level-2 Hölder-type bounds for a rough path over the alphabet Fin d with respect to a control ω. Covers non-geometric (e.g. Itô-type) rough paths: only Chen's identity and these bounds are used.

• one_third_lt : 1 / 3 < α
• le_half : α ≤ 1 / 2
• bound_one ⦃s t : ℝ⦄ : s ≤ t → ∀ (i : Fin d), ‖X.coeff s t [i]‖ₑ ≤ ω.toFun s t ^ α
• bound_two ⦃s t : ℝ⦄ : s ≤ t → ∀ (i j : Fin d), ‖X.coeff s t [i, j]‖ₑ ≤ ω.toFun s t ^ (2 * α)

theorem RoughPaths.IsLevel2RoughPath.alpha_pos {d : ℕ} {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) : 0 < α

theorem RoughPaths.IsLevel2RoughPath.one_lt_three_alpha {d : ℕ} {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} (hX : IsLevel2RoughPath X ω α) : 1 < 3 * α

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

A path with values in W controlled by the rough path X: a Gubinelli derivative Yd along the first level, a sup bound and an α-Hölder bound on the derivative, and an ω^{2α} remainder.

• Y : ℝ → W

  The underlying path.

• Yd : ℝ → Fin d → W

  The Gubinelli derivative along the first level of X.

• Cb : NNReal

  Sup bound for the derivative.

• Cd : NNReal

  Hölder constant of the derivative.

• Cy : NNReal

  Remainder constant.

• bound_Yd (s : ℝ) (i : Fin d) : ‖self.Yd s i‖ₑ ≤ ↑self.Cb
• holder_Yd ⦃s t : ℝ⦄ : s ≤ t → ∀ (i : Fin d), ‖self.Yd t i - self.Yd s i‖ₑ ≤ ↑self.Cd * ω.toFun s t ^ α
• remainder ⦃s t : ℝ⦄ : s ≤ t → ‖self.Y t - self.Y s - ∑ i : Fin d, X.coeff s t [i] • self.Yd s i‖ₑ ≤ ↑self.Cy * ω.toFun s t ^ (2 * α)

theorem RoughPaths.ControlledPath.enorm_real_smul {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (c : ℝ) (x : W) : ‖c • x‖ₑ = ‖c‖ₑ * ‖x‖ₑ

Extended-norm homogeneity of real scalar multiplication.

def RoughPaths.ControlledPath.const {d : ℕ} {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (X : AlgebraicRoughPath ℝ (Fin d) ℝ) (ω : Control ℝ) (α : ℝ) (w : W) : ControlledPath X ω α W

A constant path is controlled with zero derivative.

Equations

• RoughPaths.ControlledPath.const X ω α w = { Y := fun (x : ℝ) => w, Yd := fun (x : ℝ) (x_1 : Fin d) => 0, Cb := 0, Cd := 0, Cy := 0, bound_Yd := ⋯, holder_Yd := ⋯, remainder := ⋯ }

theorem RoughPaths.enorm_fin_sum_le {d : ℕ} {F : Type u_2} [NormedAddCommGroup F] {g : Fin d → F} {C : ENNReal} (h : ∀ (i : Fin d), ‖g i‖ₑ ≤ C) : ‖∑ i : Fin d, g i‖ₑ ≤ ↑d * C

A uniform bound on Fin d-indexed summands gives a d-scaled bound.

theorem RoughPaths.ControlledPath.enorm_increment_le {d : ℕ} {X : AlgebraicRoughPath ℝ (Fin d) ℝ} {ω : Control ℝ} {α : ℝ} {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (hX : IsLevel2RoughPath X ω α) (Z : ControlledPath X ω α W) ⦃s t : ℝ⦄ (hst : s ≤ t) : ‖Z.Y t - Z.Y s‖ₑ ≤ ↑d * ↑Z.Cb * ω.toFun s t ^ α + ↑Z.Cy * ω.toFun s t ^ (2 * α)

The path increment of a controlled path is bounded by d·Cb·ω^α + Cy·ω^{2α}.