Weakly Geometric Rough Paths

This file gives the named weakly geometric rough path layer. In the current library this is the algebraic, group-like signature-valued notion: increments satisfy Chen's identity and the shuffle identities. The metric closure definition of geometric rough paths can be added once the corresponding topology on truncated tensor algebras is available.

Main definitions

• WeakGeometricRoughPath - weakly geometric rough paths as group-like word signature increments
• ControlledWeakGeometricRoughPath - weakly geometric rough paths equipped with coordinate bounds by a control

@[reducible, inline]

abbrev RoughPaths.WeakGeometricRoughPath (T : Type u) (α : Type v) (R : Type w) [CommSemiring R] : Type (max u v w)

A weakly geometric rough path is a Hopf rough path over the word shuffle Hopf algebra: increments are characters — group-like signature series — and Chen's identity is convolution in the character monoid.

Equations

• RoughPaths.WeakGeometricRoughPath T α R = RoughPaths.HopfRoughPath (HopfAlgebras.wordHopf α).toCombBialg T R

def RoughPaths.WeakGeometricRoughPath.toAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) : AlgebraicRoughPath T α R

The underlying group-like algebraic rough path.

Equations

• X.toAlgebraic = RoughPaths.HopfRoughPath.toWord X

theorem RoughPaths.WeakGeometricRoughPath.isWeaklyGeometric {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) : X.toAlgebraic.IsWeaklyGeometric

@[implicit_reducible]

instance RoughPaths.WeakGeometricRoughPath.instCoeAlgebraicRoughPath {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] : Coe (WeakGeometricRoughPath T α R) (AlgebraicRoughPath T α R)

Equations

• RoughPaths.WeakGeometricRoughPath.instCoeAlgebraicRoughPath = { coe := fun (X : RoughPaths.WeakGeometricRoughPath T α R) => X.toAlgebraic }

def RoughPaths.WeakGeometricRoughPath.ofAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicRoughPath T α R) (hX : X.IsWeaklyGeometric) : WeakGeometricRoughPath T α R

Regard an algebraic group-like rough path as weakly geometric.

Equations

• RoughPaths.WeakGeometricRoughPath.ofAlgebraic X hX = X.toHopf hX

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.toAlgebraic_ofAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : AlgebraicRoughPath T α R) (hX : X.IsWeaklyGeometric) : (ofAlgebraic X hX).toAlgebraic = X

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.ofAlgebraic_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (h : X.toAlgebraic.IsWeaklyGeometric) : ofAlgebraic X.toAlgebraic h = X

theorem RoughPaths.WeakGeometricRoughPath.ext {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : WeakGeometricRoughPath T α R} (h : X.toAlgebraic = Y.toAlgebraic) : X = Y

theorem RoughPaths.WeakGeometricRoughPath.ext_iff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : WeakGeometricRoughPath T α R} : X = Y ↔ X.toAlgebraic = Y.toAlgebraic

def RoughPaths.WeakGeometricRoughPath.equivAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] : WeakGeometricRoughPath T α R ≃ { X : AlgebraicRoughPath T α R // X.IsWeaklyGeometric }

Weakly geometric rough paths are equivalent to group-like algebraic ones.

Equations

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

def RoughPaths.WeakGeometricRoughPath.unit (T : Type u) (α : Type v) (R : Type w) [CommSemiring R] : WeakGeometricRoughPath T α R

The constant identity weakly geometric rough path.

Equations

• RoughPaths.WeakGeometricRoughPath.unit T α R = RoughPaths.WeakGeometricRoughPath.ofAlgebraic (RoughPaths.AlgebraicRoughPath.unit T α R) ⋯

def RoughPaths.WeakGeometricRoughPath.comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : WeakGeometricRoughPath T α R) : WeakGeometricRoughPath S α R

Pull a weakly geometric rough path back along a map of time domains.

Equations

• RoughPaths.WeakGeometricRoughPath.comapTime f X = RoughPaths.WeakGeometricRoughPath.ofAlgebraic (RoughPaths.AlgebraicRoughPath.comapTime f X.toAlgebraic) ⋯

def RoughPaths.WeakGeometricRoughPath.comapMapLetters {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) : WeakGeometricRoughPath T α R

Pull a weakly geometric rough path back along a map of alphabets.

Equations

• RoughPaths.WeakGeometricRoughPath.comapMapLetters f X = RoughPaths.WeakGeometricRoughPath.ofAlgebraic (RoughPaths.AlgebraicRoughPath.comapMapLetters f X.toAlgebraic) ⋯

def RoughPaths.WeakGeometricRoughPath.increment {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) : List α → R

Signature increment of a weakly geometric rough path.

Equations

• X.increment s t = X.toAlgebraic.increment s t

def RoughPaths.WeakGeometricRoughPath.coeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) (word : List α) : R

Coordinate of a weakly geometric rough path increment on a word.

Equations

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

def RoughPaths.WeakGeometricRoughPath.truncatedIncrement {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (n : ℕ) (s t : T) : Word.Truncation α R n

Truncated signature increment of a weakly geometric rough path.

Equations

• X.truncatedIncrement n s t = X.toAlgebraic.truncatedIncrement n s t

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.toAlgebraic_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] : (unit T α R).toAlgebraic = AlgebraicRoughPath.unit T α R

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.toAlgebraic_comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : WeakGeometricRoughPath T α R) : (comapTime f X).toAlgebraic = AlgebraicRoughPath.comapTime f X.toAlgebraic

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.toAlgebraic_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) : (comapMapLetters f X).toAlgebraic = AlgebraicRoughPath.comapMapLetters f X.toAlgebraic

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.increment_apply {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) : X.increment s t = X.toAlgebraic.increment s t

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_apply {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) (word : List α) : X.coeff s t word = X.toAlgebraic.coeff s t word

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.truncatedIncrement_apply {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (n : ℕ) (s t : T) (word : { word : List α // word.length ≤ n }) : X.truncatedIncrement n s t word = X.coeff s t ↑word

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.unit_increment {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (s t : T) : (unit T α R).increment s t = Word.unit α R

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.unit_coeff_nil {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (s t : T) : (unit T α R).coeff s t [] = 1

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.unit_coeff_cons {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (s t : T) (a : α) (word : List α) : (unit T α R).coeff s t (a :: word) = 0

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : WeakGeometricRoughPath T α R) (s t : S) (word : List α) : (comapTime f X).coeff s t word = X.coeff (f s) (f t) word

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) (s t : T) (word : List α) : (comapMapLetters f X).coeff s t word = X.coeff s t (List.map f word)

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.truncatedIncrement_comapTime {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) (X : WeakGeometricRoughPath T α R) (n : ℕ) (s t : S) : (comapTime f X).truncatedIncrement n s t = X.truncatedIncrement n (f s) (f t)

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.truncatedIncrement_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) (n : ℕ) (s t : T) : (comapMapLetters f X).truncatedIncrement n s t = fun (word : { word : List α // word.length ≤ n }) => X.coeff s t (List.map f ↑word)

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.increment_self {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (t : T) : X.increment t t = Word.unit α R

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_self_nil {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (t : T) : X.coeff t t [] = 1

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_self_cons {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (t : T) (a : α) (word : List α) : X.coeff t t (a :: word) = 0

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.coeff_nil {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) : X.coeff s t [] = 1

theorem RoughPaths.WeakGeometricRoughPath.groupLike {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) : Word.IsGroupLike (X.increment s t)

theorem RoughPaths.WeakGeometricRoughPath.shuffle {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t : T) (u v : List α) : X.coeff s t u * X.coeff s t v = Word.shuffleCoeff (X.increment s t) u v

theorem RoughPaths.WeakGeometricRoughPath.chen_eq {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (s t u : T) : X.increment s u = Word.tensorProduct (X.increment s t) (X.increment t u)

@[reducible, inline]

abbrev RoughPaths.WeakGeometricRoughPath.AgreeUpToDegree {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X Y : WeakGeometricRoughPath T α R) (n : ℕ) : Prop

Agreement of weakly geometric rough paths through word degree n — the generic graded agreement of Hopf rough paths for the word-length grading.

Equations

• X.AgreeUpToDegree Y n = RoughPaths.HopfRoughPath.AgreeUpTo List.length X Y n

theorem RoughPaths.WeakGeometricRoughPath.agreeUpToDegree_iff_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X Y : WeakGeometricRoughPath T α R) (n : ℕ) : X.AgreeUpToDegree Y n ↔ X.toAlgebraic.AgreeUpToDegree Y.toAlgebraic n

theorem RoughPaths.WeakGeometricRoughPath.agreeUpToDegree_refl {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) (n : ℕ) : X.AgreeUpToDegree X n

theorem RoughPaths.WeakGeometricRoughPath.agreeUpToDegree_iff_coeff {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X Y : WeakGeometricRoughPath T α R) (n : ℕ) : X.AgreeUpToDegree Y n ↔ ∀ (s t : T) (word : List α), word.length ≤ n → X.coeff s t word = Y.coeff s t word

theorem RoughPaths.WeakGeometricRoughPath.eq_of_agreeUpToDegree_all {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {X Y : WeakGeometricRoughPath T α R} (h : ∀ (n : ℕ), X.AgreeUpToDegree Y n) : X = Y

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.comapTime_id {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) : comapTime id X = X

theorem RoughPaths.WeakGeometricRoughPath.comapTime_comp {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} {U : Type y} (f : S → T) (g : U → S) (X : WeakGeometricRoughPath T α R) : comapTime g (comapTime f X) = comapTime (f ∘ g) X

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.comapTime_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {S : Type z} (f : S → T) : comapTime f (unit T α R) = unit S α R

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.comapMapLetters_id {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] (X : WeakGeometricRoughPath T α R) : comapMapLetters id X = X

theorem RoughPaths.WeakGeometricRoughPath.comapMapLetters_comp {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} {γ : Type y} (f : α → β) (g : β → γ) (X : WeakGeometricRoughPath T γ R) : comapMapLetters f (comapMapLetters g X) = comapMapLetters (g ∘ f) X

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.comapMapLetters_unit {T : Type u} {α : Type v} {R : Type w} [CommSemiring R] {β : Type z} (f : α → β) : comapMapLetters f (unit T β R) = unit T α R

def RoughPaths.WeakGeometricRoughPath.logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] (X : WeakGeometricRoughPath T α R) (s t : T) (n : ℕ) : List α → R

Truncated log-signature increment of a weakly geometric rough path.

Equations

• X.logIncrementTruncated s t n = X.toAlgebraic.logIncrementTruncated s t n

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.logIncrementTruncated_zero {T : Type u} {α : Type v} {R : Type w} [Field R] (X : WeakGeometricRoughPath T α R) (s t : T) : X.logIncrementTruncated s t 0 = Word.zero α R

@[simp]

theorem RoughPaths.WeakGeometricRoughPath.logIncrementTruncated_self {T : Type u} {α : Type v} {R : Type w} [Field R] (X : WeakGeometricRoughPath T α R) (t : T) (n : ℕ) : X.logIncrementTruncated t t n = Word.zero α R

theorem RoughPaths.WeakGeometricRoughPath.AgreeUpToDegree.logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] {X Y : WeakGeometricRoughPath T α R} {m n : ℕ} (h : X.AgreeUpToDegree Y n) (s t : T) : Word.AgreeUpToDegree (X.logIncrementTruncated s t m) (Y.logIncrementTruncated s t m) n

theorem RoughPaths.WeakGeometricRoughPath.logIncrementTruncated_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) (s t : T) (n : ℕ) : (comapMapLetters f X).logIncrementTruncated s t n = Word.comapMapLetters f (X.logIncrementTruncated s t n)

theorem RoughPaths.WeakGeometricRoughPath.logIncrementTruncated_comapMapLetters_coeff {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : WeakGeometricRoughPath T β R) (s t : T) (n : ℕ) (word : List α) : Word.coeff ((comapMapLetters f X).logIncrementTruncated s t n) word = Word.coeff (X.logIncrementTruncated s t n) (List.map f word)

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

A controlled weakly geometric rough path with a word-coordinate bound.

• toControlled : AlgebraicRoughPath.Controlled T α R size gauge
• isWeaklyGeometric : self.toControlled.toAlgebraic.IsWeaklyGeometric

@[implicit_reducible]

instance RoughPaths.ControlledWeakGeometricRoughPath.instCoeControlled {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} : Coe (ControlledWeakGeometricRoughPath T α R size gauge) (AlgebraicRoughPath.Controlled T α R size gauge)

Equations

• RoughPaths.ControlledWeakGeometricRoughPath.instCoeControlled = { coe := fun (X : RoughPaths.ControlledWeakGeometricRoughPath T α R size gauge) => X.toControlled }

def RoughPaths.ControlledWeakGeometricRoughPath.ofControlled {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicRoughPath.Controlled T α R size gauge) (hX : X.toAlgebraic.IsWeaklyGeometric) : ControlledWeakGeometricRoughPath T α R size gauge

Regard an algebraically controlled rough path as controlled weakly geometric.

Equations

• RoughPaths.ControlledWeakGeometricRoughPath.ofControlled X hX = { toControlled := X, isWeaklyGeometric := hX }

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.toControlled_ofControlled {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicRoughPath.Controlled T α R size gauge) (hX : X.toAlgebraic.IsWeaklyGeometric) : (ofControlled X hX).toControlled = X

theorem RoughPaths.ControlledWeakGeometricRoughPath.ext {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : ControlledWeakGeometricRoughPath T α R size gauge} (h : X.toControlled = Y.toControlled) : X = Y

theorem RoughPaths.ControlledWeakGeometricRoughPath.ext_iff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : ControlledWeakGeometricRoughPath T α R size gauge} : X = Y ↔ X.toControlled = Y.toControlled

def RoughPaths.ControlledWeakGeometricRoughPath.equivControlled {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} : ControlledWeakGeometricRoughPath T α R size gauge ≃ { X : AlgebraicRoughPath.Controlled T α R size gauge // X.toAlgebraic.IsWeaklyGeometric }

Controlled weakly geometric rough paths are equivalent to controlled group-like algebraic ones.

Equations

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

def RoughPaths.ControlledWeakGeometricRoughPath.toWeakGeometric {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) : WeakGeometricRoughPath T α R

Forget the analytic control and keep the weakly geometric rough path.

Equations

• X.toWeakGeometric = RoughPaths.WeakGeometricRoughPath.ofAlgebraic X.toControlled.toAlgebraic ⋯

def RoughPaths.ControlledWeakGeometricRoughPath.toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) : AlgebraicRoughPath T α R

Underlying algebraic rough path.

Equations

• X.toAlgebraic = X.toControlled.toAlgebraic

def RoughPaths.ControlledWeakGeometricRoughPath.control {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) : Control T

The control attached to a controlled weakly geometric rough path.

Equations

• X.control = X.toControlled.control

theorem RoughPaths.ControlledWeakGeometricRoughPath.controlled {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) : X.toAlgebraic.HasCoordinateControl X.control size gauge

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

Signature coordinate of a controlled weakly geometric rough path.

Equations

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

def RoughPaths.ControlledWeakGeometricRoughPath.truncatedIncrement {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) (n : ℕ) (s t : T) : Word.Truncation α R n

Truncated increment of a controlled weakly geometric rough path.

Equations

• X.truncatedIncrement n s t = X.toWeakGeometric.truncatedIncrement n s t

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

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

Equations

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

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

Pull a controlled weakly geometric rough path back along a monotone time map.

Equations

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

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.toWeakGeometric_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) : X.toWeakGeometric.toAlgebraic = X.toAlgebraic

@[simp]

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

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.truncatedIncrement_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) (n : ℕ) (s t : T) (word : { word : List α // word.length ≤ n }) : X.truncatedIncrement n s t word = X.coeff s t ↑word

theorem RoughPaths.ControlledWeakGeometricRoughPath.coordinate_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath 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)

@[simp]

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

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.coeff_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : ControlledWeakGeometricRoughPath 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.ControlledWeakGeometricRoughPath.toControlled_comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : ControlledWeakGeometricRoughPath T α R size gauge) : (comapTime f hf X).toControlled = AlgebraicRoughPath.Controlled.comapTime f hf X.toControlled

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.coeff_comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : ControlledWeakGeometricRoughPath 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.ControlledWeakGeometricRoughPath.control_comapMapLetters {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : ControlledWeakGeometricRoughPath T β R size gauge) : (comapMapLetters f X).control = X.control

@[simp]

theorem RoughPaths.ControlledWeakGeometricRoughPath.control_comapTime {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {S : Type z} [Preorder S] (f : S → T) (hf : Monotone f) (X : ControlledWeakGeometricRoughPath T α R size gauge) : (comapTime f hf X).control = X.control.comap f hf

@[simp]

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

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

@[simp]

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

theorem RoughPaths.ControlledWeakGeometricRoughPath.comapTime_comp {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring 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 : ControlledWeakGeometricRoughPath T α R size gauge) : comapTime g hg (comapTime f hf X) = comapTime (f ∘ g) ⋯ X

def RoughPaths.ControlledWeakGeometricRoughPath.AgreeUpToDegree {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X Y : ControlledWeakGeometricRoughPath T α R size gauge) (n : ℕ) : Prop

Agreement through degree n for the underlying weakly geometric rough paths.

Equations

• X.AgreeUpToDegree Y n = X.toWeakGeometric.AgreeUpToDegree Y.toWeakGeometric n

theorem RoughPaths.ControlledWeakGeometricRoughPath.agreeUpToDegree_refl {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : ControlledWeakGeometricRoughPath T α R size gauge) (n : ℕ) : X.AgreeUpToDegree X n

theorem RoughPaths.ControlledWeakGeometricRoughPath.agreeUpToDegree_iff_coeff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X Y : ControlledWeakGeometricRoughPath T α R size gauge) (n : ℕ) : X.AgreeUpToDegree Y n ↔ ∀ (s t : T) (word : List α), word.length ≤ n → X.coeff s t word = Y.coeff s t word

theorem RoughPaths.ControlledWeakGeometricRoughPath.toWeakGeometric_eq_of_agreeUpToDegree_all {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : ControlledWeakGeometricRoughPath T α R size gauge} (h : ∀ (n : ℕ), X.AgreeUpToDegree Y n) : X.toWeakGeometric = Y.toWeakGeometric

theorem RoughPaths.ControlledWeakGeometricRoughPath.agreeUpToDegree_all_iff_toWeakGeometric_eq {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : ControlledWeakGeometricRoughPath T α R size gauge} : (∀ (n : ℕ), X.AgreeUpToDegree Y n) ↔ X.toWeakGeometric = Y.toWeakGeometric