Concrete rough paths

The first genuine instances connecting the algebraic and analytic halves of the library:

• AlgebraicRoughPath.ofLinear — the canonical (signature) lift of the linear path t ↦ t·v, a weakly geometric rough path over any field;
• AlgebraicRoughPath.ofLinearClamped — its clamp to the time window [0, T₀], which satisfies the global level-2 Hölder bounds IsLevel2RoughPath with α = 1/2 against the linear control Control.ofReal (M²·T₀) — so the entire rough integration and RDE theory applies to it;
• AlgebraicRoughPath.bracketPath — the Itô-type bracket path exp((t-s)·(e₀⊗e₀)): zero first level, symmetric second level t-s. Chen's identity holds (the binomial law for the tensor exponential) but the shuffle identity fails, so it is a genuinely non-geometric rough path; it is nevertheless level-2 with α = 1/2.

noncomputable def RoughPaths.clampTo (T₀ r : ℝ) : ℝ

Clamp a real time to the window [0, T₀].

Equations

• RoughPaths.clampTo T₀ r = min (max r 0) T₀

theorem RoughPaths.clampTo_mono (T₀ : ℝ) : Monotone (clampTo T₀)

theorem RoughPaths.clampTo_nonneg {T₀ : ℝ} (hT₀ : 0 ≤ T₀) (r : ℝ) : 0 ≤ clampTo T₀ r

theorem RoughPaths.clampTo_le (T₀ r : ℝ) : clampTo T₀ r ≤ T₀

theorem RoughPaths.clampTo_le_add (T₀ : ℝ) {s t : ℝ} (h : s ≤ t) : clampTo T₀ t ≤ clampTo T₀ s + (t - s)

The clamp is 1-Lipschitz from the left.

def RoughPaths.AlgebraicRoughPath.ofLinear {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) : AlgebraicRoughPath R α R

The canonical rough-path lift of the linear path t ↦ t·v: increments are the linear signatures of the scaled segment. Chen's identity is the semigroup law tensorProduct_linearSignature_smul.

Equations

• RoughPaths.AlgebraicRoughPath.ofLinear v = { increment := fun (s t : R) => RoughPaths.Word.linearSignature ((t - s) • v), identity := ⋯, chen := ⋯, unitEmpty := ⋯ }

@[simp]

theorem RoughPaths.AlgebraicRoughPath.ofLinear_increment {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) (s t : R) : (ofLinear v).increment s t = Word.linearSignature ((t - s) • v)

theorem RoughPaths.AlgebraicRoughPath.ofLinear_isWeaklyGeometric {α : Type u} {R : Type v} [Field R] [CharZero R] (v : α → R) : (ofLinear v).IsWeaklyGeometric

The signature lift of a linear path is weakly geometric.

noncomputable def RoughPaths.AlgebraicRoughPath.ofLinearClamped {d : ℕ} (v : Fin d → ℝ) (T₀ : ℝ) : AlgebraicRoughPath ℝ (Fin d) ℝ

The linear path clamped to the window [0, T₀]: constant before 0, linear on [0, T₀], constant after. Unlike the unclamped lift it carries global level-2 bounds.

Equations

• RoughPaths.AlgebraicRoughPath.ofLinearClamped v T₀ = RoughPaths.AlgebraicRoughPath.comapTime (RoughPaths.clampTo T₀) (RoughPaths.AlgebraicRoughPath.ofLinear v)

theorem RoughPaths.AlgebraicRoughPath.ofLinearClamped_isWeaklyGeometric {d : ℕ} (v : Fin d → ℝ) (T₀ : ℝ) : (ofLinearClamped v T₀).IsWeaklyGeometric

theorem RoughPaths.AlgebraicRoughPath.ofLinearClamped_coeff_single {d : ℕ} (v : Fin d → ℝ) (T₀ s t : ℝ) (i : Fin d) : (ofLinearClamped v T₀).coeff s t [i] = (clampTo T₀ t - clampTo T₀ s) * v i

theorem RoughPaths.AlgebraicRoughPath.ofLinearClamped_coeff_pair {d : ℕ} (v : Fin d → ℝ) (T₀ s t : ℝ) (i j : Fin d) : (ofLinearClamped v T₀).coeff s t [i, j] = (clampTo T₀ t - clampTo T₀ s) * v i * ((clampTo T₀ t - clampTo T₀ s) * v j) / 2

theorem RoughPaths.AlgebraicRoughPath.ofLinearClamped_isLevel2 {d : ℕ} (v : Fin d → ℝ) {M T₀ : ℝ} (hT₀ : 0 ≤ T₀) (hM : 0 ≤ M) (hv : ∀ (i : Fin d), |v i| ≤ M) : IsLevel2RoughPath (ofLinearClamped v T₀) (Control.ofReal (ENNReal.ofReal (M ^ 2 * T₀))) (1 / 2)

The clamped linear path is a global level-2 rough path with α = 1/2 against the linear control ω = (M²T₀)·(t-s): the first end-to-end analytic instance of the theory.

The bracket path: a non-geometric rough path

noncomputable def RoughPaths.AlgebraicRoughPath.bracketCoeff (a : ℝ) (k : ℕ) : ℝ

The coefficient profile of the bracket path: aᵐ/m! on words of length 2m, zero on odd lengths.

Equations

• RoughPaths.AlgebraicRoughPath.bracketCoeff a k = if 2 ∣ k then a ^ (k / 2) / ↑(k / 2).factorial else 0

theorem RoughPaths.AlgebraicRoughPath.bracketCoeff_even (a : ℝ) (m : ℕ) : bracketCoeff a (2 * m) = a ^ m / ↑m.factorial

theorem RoughPaths.AlgebraicRoughPath.bracketCoeff_odd (a : ℝ) {k : ℕ} (h : ¬2 ∣ k) : bracketCoeff a k = 0

theorem RoughPaths.AlgebraicRoughPath.bracketCoeff_zero_left (k : ℕ) (hk : k ≠ 0) : bracketCoeff 0 k = 0

noncomputable def RoughPaths.AlgebraicRoughPath.bracketPath : AlgebraicRoughPath ℝ (Fin 1) ℝ

The bracket path: the Itô-type lift of a constant path — zero first level, symmetric second level X²(s,t) = t-s. It is the tensor exponential exp((t-s)·(e₀⊗e₀)), so Chen's identity is the binomial law; the shuffle identity fails at level one (see bracketPath_not_isWeaklyGeometric).

Equations

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

@[simp]

theorem RoughPaths.AlgebraicRoughPath.bracketPath_coeff (s t : ℝ) (w : List (Fin 1)) : bracketPath.coeff s t w = bracketCoeff (t - s) w.length

theorem RoughPaths.AlgebraicRoughPath.bracketPath_not_isWeaklyGeometric : ¬bracketPath.IsWeaklyGeometric

The bracket path is not weakly geometric: the shuffle identity fails at the first level, 2·X²₀₀ = 2·(t-s) ≠ 0 = X¹₀·X¹₀. Together with bracketPath (Chen holds) this exhibits a genuinely non-geometric rough path, as promised by the non-geometric base of the theory.

theorem RoughPaths.AlgebraicRoughPath.bracketPath_isLevel2 : IsLevel2RoughPath bracketPath (Control.ofReal 1) (1 / 2)

The bracket path is level-2 with α = 1/2 against ω = t-s: a complete non-geometric instance of the analytic theory.