Concrete controls

Constructions of superadditive controls: the linear control c·(t − s) on the real line, sums, scalar multiples, powers ω^p for p ≥ 1, controls from bounded variation, and the bridge from Hölder continuity. Also the standard power gauge (k, r) ↦ C^k · r^(a·k) instantiating the abstract gauge of RoughPaths.Analytic.

noncomputable def RoughPaths.Control.ofReal (c : ENNReal) : Control ℝ

The linear control c·(t − s) on the real line.

Equations

• RoughPaths.Control.ofReal c = { toFun := fun (s t : ℝ) => c * ENNReal.ofReal (t - s), diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.ofReal_apply (c : ENNReal) (s t : ℝ) : (ofReal c).toFun s t = c * ENNReal.ofReal (t - s)

def RoughPaths.Control.add {T : Type u} [Preorder T] (ω η : Control T) : Control T

The sum of two controls.

Equations

• ω.add η = { toFun := fun (s t : T) => ω.toFun s t + η.toFun s t, diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.add_apply {T : Type u} [Preorder T] (ω η : Control T) (s t : T) : (ω.add η).toFun s t = ω.toFun s t + η.toFun s t

noncomputable def RoughPaths.Control.constMul {T : Type u} [Preorder T] (c : ENNReal) (ω : Control T) : Control T

A scalar multiple of a control.

Equations

• RoughPaths.Control.constMul c ω = { toFun := fun (s t : T) => c * ω.toFun s t, diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.constMul_apply {T : Type u} [Preorder T] (c : ENNReal) (ω : Control T) (s t : T) : (constMul c ω).toFun s t = c * ω.toFun s t

noncomputable def RoughPaths.Control.rpow {T : Type u} [Preorder T] (ω : Control T) (p : ℝ) (hp : 1 ≤ p) : Control T

The p-th power of a control is a control for p ≥ 1.

Equations

• ω.rpow p hp = { toFun := fun (s t : T) => ω.toFun s t ^ p, diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.rpow_apply {T : Type u} [Preorder T] (ω : Control T) (p : ℝ) (hp : 1 ≤ p) (s t : T) : (ω.rpow p hp).toFun s t = ω.toFun s t ^ p

noncomputable def RoughPaths.Control.ofEVariation {E : Type v} [PseudoEMetricSpace E] (f : ℝ → E) : Control ℝ

The control given by the extended variation of a path on [s, t].

Equations

• RoughPaths.Control.ofEVariation f = { toFun := fun (s t : ℝ) => if s ≤ t then eVariationOn f (Set.Icc s t) else 0, diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.ofEVariation_apply_of_le {E : Type v} [PseudoEMetricSpace E] (f : ℝ → E) {s t : ℝ} (hst : s ≤ t) : (ofEVariation f).toFun s t = eVariationOn f (Set.Icc s t)

noncomputable def RoughPaths.Control.holder (C r : NNReal) : Control ℝ

The linear control associated with a (C, r)-Hölder bound: the control stays LINEAR (so fine partitions are free) and the Hölder exponent lives in the sewing exponent θ.

Equations

• RoughPaths.Control.holder C r = RoughPaths.Control.ofReal (↑C ^ (1 / ↑r))

theorem RoughPaths.Control.holder_bound {E : Type v} [SeminormedAddCommGroup E] {C r : NNReal} (hr : 0 < r) {f : ℝ → E} (hf : HolderWith C r f) {s t : ℝ} (hst : s ≤ t) : ‖f t - f s‖ₑ ≤ (holder C r).toFun s t ^ ↑r

A (C, r)-Hölder path has increments bounded by (holder C r) ^ r.

noncomputable def RoughPaths.powGauge (C : ENNReal) (a : ℝ) : ℕ → ENNReal → ENNReal

The standard power gauge (k, r) ↦ C^k · r^(a·k) bounding the word coordinates of a rough path of regularity a.

Equations

• RoughPaths.powGauge C a k r = C ^ k * r ^ (a * ↑k)

@[simp]

theorem RoughPaths.powGauge_apply (C : ENNReal) (a : ℝ) (k : ℕ) (r : ENNReal) : powGauge C a k r = C ^ k * r ^ (a * ↑k)