The topology on level-2 rough paths

The space Level2RoughPath ω α d of rough paths carrying level-2 bounds against a fixed control ω, with the inhomogeneous rough path distance

ϱ(X,X') = sup_{s≤t} max( ‖X¹-X'¹‖ₑ/ω^α , ‖X²-X'²‖ₑ/ω^{2α} ).

This is a pseudo-emetric: two rough paths at distance zero agree at levels one and two wherever ω is positive but may differ at higher levels. Since both arguments obey the same level-2 bounds the distance is bounded by 2 on the whole space.

RoughPathDist is the certified-constants form of the same distance used by the quantitative stability theory; the two are interchangeable via edist_le_of_roughPathDist and RoughPathDist.of_edist_le.

structure RoughPaths.RoughPathDist {d : ℕ} (X X' : AlgebraicRoughPath ℝ (Fin d) ℝ) (ω : Control ℝ) (α : ℝ) (ρ₁ ρ₂ : NNReal) : Prop

Certified distance between two rough paths over the same control: ρ₁·ω^α at the first level and ρ₂·ω^{2α} at the second.

• bound_one ⦃s t : ℝ⦄ : s ≤ t → ∀ (i : Fin d), ‖X.coeff s t [i] - X'.coeff s t [i]‖ₑ ≤ ↑ρ₁ * ω.toFun s t ^ α
• bound_two ⦃s t : ℝ⦄ : s ≤ t → ∀ (i j : Fin d), ‖X.coeff s t [i, j] - X'.coeff s t [i, j]‖ₑ ≤ ↑ρ₂ * ω.toFun s t ^ (2 * α)

structure RoughPaths.Level2RoughPath (ω : Control ℝ) (α : ℝ) (d : ℕ) : Type

The space of level-2 rough paths over a fixed control and exponent: the carrier of the rough path topology.

• X : AlgebraicRoughPath ℝ (Fin d) ℝ

  The underlying algebraic rough path.

• level2 : IsLevel2RoughPath self.X ω α

  The level-2 Hölder certificate.

noncomputable def RoughPaths.Level2RoughPath.roughDist {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) : ENNReal

The inhomogeneous rough path distance.

Equations

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

theorem RoughPaths.Level2RoughPath.term_le_roughDist_one {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) {s t : ℝ} (hst : s ≤ t) (i : Fin d) : ‖A.X.coeff s t [i] - B.X.coeff s t [i]‖ₑ / ω.toFun s t ^ α ≤ A.roughDist B

theorem RoughPaths.Level2RoughPath.term_le_roughDist_two {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) {s t : ℝ} (hst : s ≤ t) (i j : Fin d) : ‖A.X.coeff s t [i, j] - B.X.coeff s t [i, j]‖ₑ / ω.toFun s t ^ (2 * α) ≤ A.roughDist B

@[implicit_reducible]

noncomputable instance RoughPaths.Level2RoughPath.instPseudoEMetricSpace {d : ℕ} {ω : Control ℝ} {α : ℝ} : PseudoEMetricSpace (Level2RoughPath ω α d)

The rough path topology: the space of level-2 rough paths is a pseudo-emetric space under the inhomogeneous rough path distance.

Equations

• RoughPaths.Level2RoughPath.instPseudoEMetricSpace = { edist := RoughPaths.Level2RoughPath.roughDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, uniformity_edist := ⋯ }

theorem RoughPaths.Level2RoughPath.edist_def {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) : edist A B = A.roughDist B

theorem RoughPaths.Level2RoughPath.edist_le_two {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) : edist A B ≤ 2

The rough path distance is bounded by 2 on the whole space: both arguments obey the same level-2 bounds.

theorem RoughPaths.Level2RoughPath.edist_ne_top {d : ℕ} {ω : Control ℝ} {α : ℝ} (A B : Level2RoughPath ω α d) : edist A B ≠ ⊤

theorem RoughPaths.Level2RoughPath.edist_le_of_roughPathDist {d : ℕ} {ω : Control ℝ} {α : ℝ} {A B : Level2RoughPath ω α d} {ρ₁ ρ₂ : NNReal} (h : RoughPathDist A.X B.X ω α ρ₁ ρ₂) : edist A B ≤ max ↑ρ₁ ↑ρ₂

A certified rough path distance bounds the metric distance.

theorem RoughPaths.Level2RoughPath.RoughPathDist.of_edist_le {d : ℕ} {ω : Control ℝ} {α : ℝ} {A B : Level2RoughPath ω α d} {ρ : NNReal} (hα : 0 ≤ α) (hω : ∀ ⦃s t : ℝ⦄, s ≤ t → ω.toFun s t ≠ ⊤) (h : edist A B ≤ ↑ρ) : RoughPathDist A.X B.X ω α ρ ρ

A metric distance bound certifies the rough path distance (the control must be finite to unfold the division).