Analytic Rough Path Bounds

This file adds a lightweight analytic layer for rough paths. The central object is a control, a superadditive two-parameter function used in the standard formulation of rough path variation estimates.

The bounds are deliberately stated with an abstract coordinate size and gauge. This keeps the definitions independent of a particular normed coefficient space or choice of exponent.

Main definitions

• Control - superadditive two-parameter control function
• IncrementControlledBy - generic bound for an increment map
• AlgebraicRoughPath.HasCoordinateControl - word-coordinate bounds

Forest-coordinate controls for branched rough paths live downstream in LeanBSeries (BSeries.RoughPaths.Analytic).

structure RoughPaths.Control (T : Type u) [Preorder T] : Type u

A control is a superadditive two-parameter function with zero diagonal.

• toFun : T → T → ENNReal
• diagonal (t : T) : self.toFun t t = 0
• superadditive {s u t : T} : s ≤ u → u ≤ t → self.toFun s u + self.toFun u t ≤ self.toFun s t

@[implicit_reducible]

instance RoughPaths.Control.instCoeFunForallForallENNReal {T : Type u} [Preorder T] : CoeFun (Control T) fun (x : Control T) => T → T → ENNReal

Equations

• RoughPaths.Control.instCoeFunForallForallENNReal = { coe := fun (ω : RoughPaths.Control T) => ω.toFun }

theorem RoughPaths.Control.ext {T : Type u} [Preorder T] {ω η : Control T} (h : ∀ (s t : T), ω.toFun s t = η.toFun s t) : ω = η

theorem RoughPaths.Control.ext_iff {T : Type u} [Preorder T] {ω η : Control T} : ω = η ↔ ∀ (s t : T), ω.toFun s t = η.toFun s t

@[simp]

theorem RoughPaths.Control.diagonal_apply {T : Type u} [Preorder T] (ω : Control T) (t : T) : ω.toFun t t = 0

theorem RoughPaths.Control.superadditive_apply {T : Type u} [Preorder T] (ω : Control T) {s u t : T} (hsu : s ≤ u) (hut : u ≤ t) : ω.toFun s u + ω.toFun u t ≤ ω.toFun s t

def RoughPaths.Control.zero (T : Type u) [Preorder T] : Control T

The zero control.

Equations

• RoughPaths.Control.zero T = { toFun := fun (x x_1 : T) => 0, diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.zero_apply {T : Type u} [Preorder T] (s t : T) : (zero T).toFun s t = 0

def RoughPaths.Control.comap {S : Type z} {T : Type u} [Preorder S] [Preorder T] (ω : Control T) (f : S → T) (hf : Monotone f) : Control S

Pull a control back along a monotone map of time domains.

Equations

• ω.comap f hf = { toFun := fun (s t : S) => ω.toFun (f s) (f t), diagonal := ⋯, superadditive := ⋯ }

@[simp]

theorem RoughPaths.Control.comap_apply {S : Type z} {T : Type u} [Preorder S] [Preorder T] (ω : Control T) (f : S → T) (hf : Monotone f) (s t : S) : (ω.comap f hf).toFun s t = ω.toFun (f s) (f t)

@[simp]

theorem RoughPaths.Control.comap_id {T : Type u} [Preorder T] (ω : Control T) : ω.comap id ⋯ = ω

theorem RoughPaths.Control.comap_comp {S : Type z} {T : Type u} [Preorder S] [Preorder T] {U : Type y} [Preorder U] (ω : Control T) (f : S → T) (hf : Monotone f) (g : U → S) (hg : Monotone g) : (ω.comap f hf).comap g hg = ω.comap (f ∘ g) ⋯

def RoughPaths.IncrementControlledBy {T : Type u} {E : Type v} [Preorder T] (x : T → T → E) (size : E → ENNReal) (ω : Control T) : Prop

A generic coordinate increment bound by a control.

Equations

• RoughPaths.IncrementControlledBy x size ω = ∀ {s t : T}, s ≤ t → size (x s t) ≤ ω.toFun s t

theorem RoughPaths.IncrementControlledBy.mono_control {T : Type u} {E : Type v} [Preorder T] {x : T → T → E} {size : E → ENNReal} {ω η : Control T} (h : IncrementControlledBy x size ω) (hω : ∀ {s t : T}, s ≤ t → ω.toFun s t ≤ η.toFun s t) : IncrementControlledBy x size η

theorem RoughPaths.IncrementControlledBy.mono_size {T : Type u} {E : Type v} [Preorder T] {x : T → T → E} {size size' : E → ENNReal} {ω : Control T} (h : IncrementControlledBy x size ω) (hsize : ∀ (y : E), size' y ≤ size y) : IncrementControlledBy x size' ω

theorem RoughPaths.IncrementControlledBy.comapTime {T : Type u} {E : Type v} [Preorder T] {S : Type z} [Preorder S] {x : T → T → E} {size : E → ENNReal} {ω : Control T} (h : IncrementControlledBy x size ω) (f : S → T) (hf : Monotone f) : IncrementControlledBy (fun (s t : S) => x (f s) (f t)) size (ω.comap f hf)

def RoughPaths.AlgebraicRoughPath.HasCoordinateControl {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] (X : AlgebraicRoughPath T α R) (ω : Control T) (size : R → ENNReal) (gauge : ℕ → ENNReal → ENNReal) : Prop

All word coordinates of a rough path are bounded by a control and gauge.

Equations

• X.HasCoordinateControl ω size gauge = ∀ {s t : T}, s ≤ t → ∀ (word : List α), size (X.coeff s t word) ≤ gauge word.length (ω.toFun s t)

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.coeff_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {X : AlgebraicRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) {s t : T} (hst : s ≤ t) (word : List α) : size (X.coeff s t word) ≤ gauge word.length (ω.toFun s t)

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.incrementControlledBy {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {X : AlgebraicRoughPath T α R} {ω η : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) (word : List α) (hη : ∀ {s t : T}, s ≤ t → gauge word.length (ω.toFun s t) ≤ η.toFun s t) : IncrementControlledBy (fun (s t : T) => X.coeff s t word) size η

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {β : Type z} (f : α → β) {X : AlgebraicRoughPath T β R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) : (AlgebraicRoughPath.comapMapLetters f X).HasCoordinateControl ω size gauge

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) {X : AlgebraicRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) : (AlgebraicRoughPath.comapTime f X).HasCoordinateControl (ω.comap f hf) size gauge

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.mono_gauge {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {X : AlgebraicRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge gauge' : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) (hgauge : ∀ (n : ℕ) (r : ENNReal), gauge n r ≤ gauge' n r) : X.HasCoordinateControl ω size gauge'

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.mono_size {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {X : AlgebraicRoughPath T α R} {ω : Control T} {size size' : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) (hsize : ∀ (r : R), size' r ≤ size r) : X.HasCoordinateControl ω size' gauge

theorem RoughPaths.AlgebraicRoughPath.HasCoordinateControl.mono_control {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {X : AlgebraicRoughPath T α R} {ω η : Control T} {size : R → ENNReal} {gauge gauge' : ℕ → ENNReal → ENNReal} (h : X.HasCoordinateControl ω size gauge) (hω : ∀ {s t : T}, s ≤ t → ω.toFun s t ≤ η.toFun s t) (hgauge : ∀ (n : ℕ) {r r' : ENNReal}, r ≤ r' → gauge n r ≤ gauge' n r') : X.HasCoordinateControl η size gauge'

structure RoughPaths.AlgebraicRoughPath.Controlled (T : Type u) (α : Type v) (R : Type w) [Preorder T] [Semiring R] (size : R → ENNReal) (gauge : ℕ → ENNReal → ENNReal) : Type (max (max u v) w)

A rough path together with a coordinate control certificate.

• toAlgebraic : AlgebraicRoughPath T α R
• control : Control T
• controlled : self.toAlgebraic.HasCoordinateControl self.control size gauge

theorem RoughPaths.AlgebraicRoughPath.Controlled.ext {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : Controlled T α R size gauge} (halg : X.toAlgebraic = Y.toAlgebraic) (hcontrol : X.control = Y.control) : X = Y

theorem RoughPaths.AlgebraicRoughPath.Controlled.ext_iff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : Controlled T α R size gauge} : X = Y ↔ X.toAlgebraic = Y.toAlgebraic ∧ X.control = Y.control

def RoughPaths.AlgebraicRoughPath.Controlled.comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : Controlled T β R size gauge) : Controlled T α R size gauge

Pull a controlled rough path back along a map of alphabets.

Equations

• RoughPaths.AlgebraicRoughPath.Controlled.comapMapLetters f X = { toAlgebraic := RoughPaths.AlgebraicRoughPath.comapMapLetters f X.toAlgebraic, control := X.control, controlled := ⋯ }

def RoughPaths.AlgebraicRoughPath.Controlled.comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : Controlled T α R size gauge) : Controlled S α R size gauge

Pull a controlled rough path back along a monotone map of time domains.

Equations

• RoughPaths.AlgebraicRoughPath.Controlled.comapTime f hf X = { toAlgebraic := RoughPaths.AlgebraicRoughPath.comapTime f X.toAlgebraic, control := X.control.comap f hf, controlled := ⋯ }

def RoughPaths.AlgebraicRoughPath.Controlled.coeff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (word : List α) : R

Coordinate of a controlled rough path increment on a word.

Equations

• X.coeff s t word = X.toAlgebraic.coeff s t word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapMapLetters_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : Controlled T β R size gauge) : (comapMapLetters f X).toAlgebraic = AlgebraicRoughPath.comapMapLetters f X.toAlgebraic

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.coeff_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (word : List α) : X.coeff s t word = X.toAlgebraic.coeff s t word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.coeff_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : Controlled T β R size gauge) (s t : T) (word : List α) : (comapMapLetters f X).coeff s t word = X.coeff s t (List.map f word)

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapTime_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : Controlled T α R size gauge) : (comapTime f hf X).toAlgebraic = AlgebraicRoughPath.comapTime f X.toAlgebraic

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.coeff_comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : Controlled T α R size gauge) (s t : S) (word : List α) : (comapTime f hf X).coeff s t word = X.coeff (f s) (f t) word

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapMapLetters_id {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) : comapMapLetters id X = X

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapMapLetters_comp {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} {γ : Type y} (f : α → β) (g : β → γ) (X : Controlled T γ R size gauge) : comapMapLetters f (comapMapLetters g X) = comapMapLetters (g ∘ f) X

@[simp]

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapTime_id {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) : comapTime id ⋯ X = X

theorem RoughPaths.AlgebraicRoughPath.Controlled.comapTime_comp {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} {U : Type y} [Preorder S] [Preorder U] (f : S → T) (hf : Monotone f) (g : U → S) (hg : Monotone g) (X : Controlled T α R size gauge) : comapTime g hg (comapTime f hf X) = comapTime (f ∘ g) ⋯ X

theorem RoughPaths.AlgebraicRoughPath.Controlled.coordinate_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [Semiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) {s t : T} (hst : s ≤ t) (word : List α) : size (X.coeff s t word) ≤ gauge word.length (X.control.toFun s t)