Analytic control of branched rough paths

Forest-coordinate controls (HasForestControl) for branched and labelled branched rough paths, extending the geometric controls of RoughPaths.Analytic.

def RoughPaths.AlgebraicBranchedRoughPath.HasForestControl {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] (X : AlgebraicBranchedRoughPath T R) (ω : Control T) (size : R → ENNReal) (gauge : ℕ → ENNReal → ENNReal) : Prop

All forest coordinates of a branched rough path are bounded by a control.

Equations

• X.HasForestControl ω size gauge = ∀ {s t : T}, s ≤ t → ∀ (φ : HopfAlgebras.RootedForest), size (RoughPaths.HopfRoughPath.coeff X s t φ) ≤ gauge φ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicBranchedRoughPath.HasForestControl.coeff_bound {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) {s t : T} (hst : s ≤ t) (φ : HopfAlgebras.RootedForest) : size (HopfRoughPath.coeff X s t φ) ≤ gauge φ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicBranchedRoughPath.HasForestControl.incrementControlledBy {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω η : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) (φ : HopfAlgebras.RootedForest) (hη : ∀ {s t : T}, s ≤ t → gauge φ.order (ω.toFun s t) ≤ η.toFun s t) : IncrementControlledBy (fun (s t : T) => HopfRoughPath.coeff X s t φ) size η

theorem RoughPaths.AlgebraicBranchedRoughPath.HasForestControl.treeCoeff_bound {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) {s t : T} (hst : s ≤ t) (τ : HopfAlgebras.RootedTree) : size (X.treeCoeff s t τ) ≤ gauge τ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicBranchedRoughPath.HasForestControl.treeIncrementControlledBy {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω η : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) (τ : HopfAlgebras.RootedTree) (hη : ∀ {s t : T}, s ≤ t → gauge τ.order (ω.toFun s t) ≤ η.toFun s t) : IncrementControlledBy (fun (s t : T) => X.treeCoeff s t τ) size η

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

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

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

theorem RoughPaths.AlgebraicBranchedRoughPath.HasForestControl.mono_control {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω η : Control T} {size : R → ENNReal} {gauge gauge' : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω 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.HasForestControl η size gauge'

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

A branched rough path together with a forest-coordinate control certificate.

• toAlgebraic : AlgebraicBranchedRoughPath T R
• control : Control T
• controlled : self.toAlgebraic.HasForestControl self.control size gauge

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.ext {T : Type u} {R : Type v} [Preorder T] [CommSemiring 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.AlgebraicBranchedRoughPath.Controlled.ext_iff {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : Controlled T R size gauge} : X = Y ↔ X.toAlgebraic = Y.toAlgebraic ∧ X.control = Y.control

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.Controlled.comapTime {T : Type u} {R : Type v} [Preorder T] [CommSemiring 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 branched rough path back along a monotone map of time domains.

Equations

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

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.Controlled.coeff {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) (s t : T) (φ : HopfAlgebras.RootedForest) : R

Coordinate of a controlled branched rough path increment on a forest.

Equations

• X.coeff s t φ = RoughPaths.HopfRoughPath.coeff X.toAlgebraic s t φ

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.Controlled.treeCoeff {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) (s t : T) (τ : HopfAlgebras.RootedTree) : R

Coordinate of a controlled branched rough path increment on a tree.

Equations

• X.treeCoeff s t τ = X.toAlgebraic.treeCoeff s t τ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.coeff_apply {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) (s t : T) (φ : HopfAlgebras.RootedForest) : X.coeff s t φ = HopfRoughPath.coeff X.toAlgebraic s t φ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.treeCoeff_apply {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) (s t : T) (τ : HopfAlgebras.RootedTree) : X.treeCoeff s t τ = X.toAlgebraic.treeCoeff s t τ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.comapTime_toAlgebraic {T : Type u} {R : Type v} [Preorder T] [CommSemiring 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 = AlgebraicBranchedRoughPath.comapTime f X.toAlgebraic

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.coeff_comapTime {T : Type u} {R : Type v} [Preorder T] [CommSemiring 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) (φ : HopfAlgebras.RootedForest) : (comapTime f hf X).coeff s t φ = X.coeff (f s) (f t) φ

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.treeCoeff_comapTime {T : Type u} {R : Type v} [Preorder T] [CommSemiring 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) (τ : HopfAlgebras.RootedTree) : (comapTime f hf X).treeCoeff s t τ = X.treeCoeff (f s) (f t) τ

@[simp]

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

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

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.coordinate_bound {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) {s t : T} (hst : s ≤ t) (φ : HopfAlgebras.RootedForest) : size (X.coeff s t φ) ≤ gauge φ.order (X.control.toFun s t)

theorem RoughPaths.AlgebraicBranchedRoughPath.Controlled.tree_coordinate_bound {T : Type u} {R : Type v} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T R size gauge) {s t : T} (hst : s ≤ t) (τ : HopfAlgebras.RootedTree) : size (X.treeCoeff s t τ) ≤ gauge τ.order (X.control.toFun s t)

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

All labelled forest coordinates are bounded by a control and gauge.

Equations

• X.HasForestControl ω size gauge = ∀ {s t : T}, s ≤ t → ∀ (φ : HopfAlgebras.LRootedForest α), size (RoughPaths.HopfRoughPath.coeff X s t φ) ≤ gauge φ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.coeff_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) {s t : T} (hst : s ≤ t) (φ : HopfAlgebras.LRootedForest α) : size (HopfRoughPath.coeff X s t φ) ≤ gauge φ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.incrementControlledBy {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} {ω η : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) (φ : HopfAlgebras.LRootedForest α) (hη : ∀ {s t : T}, s ≤ t → gauge φ.order (ω.toFun s t) ≤ η.toFun s t) : IncrementControlledBy (fun (s t : T) => HopfRoughPath.coeff X s t φ) size η

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.treeCoeff_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) {s t : T} (hst : s ≤ t) (τ : HopfAlgebras.LRootedTree α) : size (X.treeCoeff s t τ) ≤ gauge τ.order (ω.toFun s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.treeIncrementControlledBy {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} {ω η : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) (τ : HopfAlgebras.LRootedTree α) (hη : ∀ {s t : T}, s ≤ t → gauge τ.order (ω.toFun s t) ≤ η.toFun s t) : IncrementControlledBy (fun (s t : T) => X.treeCoeff s t τ) size η

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.comapMapLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {β : Type z} (f : α → β) {X : AlgebraicLabelledBranchedRoughPath T β R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) : (AlgebraicLabelledBranchedRoughPath.comapMapLabels f X).HasForestControl ω size gauge

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicBranchedRoughPath T R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) : (AlgebraicLabelledBranchedRoughPath.comapEraseLabels X).HasForestControl ω size gauge

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] (a : α) {X : AlgebraicLabelledBranchedRoughPath T α R} {ω : Control T} {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω size gauge) : (AlgebraicLabelledBranchedRoughPath.comapConstLabel a X).HasForestControl ω size gauge

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

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

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

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.HasForestControl.mono_control {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {X : AlgebraicLabelledBranchedRoughPath T α R} {ω η : Control T} {size : R → ENNReal} {gauge gauge' : ℕ → ENNReal → ENNReal} (h : X.HasForestControl ω 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.HasForestControl η size gauge'

structure RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled (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 labelled branched rough path with a forest-coordinate control certificate.

• toAlgebraic : AlgebraicLabelledBranchedRoughPath T α R
• control : Control T
• controlled : self.toAlgebraic.HasForestControl self.control size gauge

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.ext {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring 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.AlgebraicLabelledBranchedRoughPath.Controlled.ext_iff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X Y : Controlled T α R size gauge} : X = Y ↔ X.toAlgebraic = Y.toAlgebraic ∧ X.control = Y.control

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

Pull a controlled labelled branched rough path back along a relabelling map.

Equations

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) : Controlled T α R size gauge

Pull an unlabelled controlled branched rough path back to labelled forests.

Equations

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (a : α) (X : Controlled T α R size gauge) : AlgebraicBranchedRoughPath.Controlled T R size gauge

Restrict a labelled controlled branched rough path to one constant label.

Equations

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.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 : Controlled T α R size gauge) : Controlled S α R size gauge

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

Equations

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

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coeff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (φ : HopfAlgebras.LRootedForest α) : R

Coordinate of a controlled labelled branched rough path on a forest.

Equations

• X.coeff s t φ = RoughPaths.HopfRoughPath.coeff X.toAlgebraic s t φ

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (τ : HopfAlgebras.LRootedTree α) : R

Coordinate of a controlled labelled branched rough path on a tree.

Equations

• X.treeCoeff s t τ = X.toAlgebraic.treeCoeff s t τ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coeff_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (φ : HopfAlgebras.LRootedForest α) : X.coeff s t φ = HopfRoughPath.coeff X.toAlgebraic s t φ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) (s t : T) (τ : HopfAlgebras.LRootedTree α) : X.treeCoeff s t τ = X.toAlgebraic.treeCoeff s t τ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coeff_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : Controlled T β R size gauge) (s t : T) (φ : HopfAlgebras.LRootedForest α) : (comapMapLabels f X).coeff s t φ = X.coeff s t (HopfAlgebras.LRootedForest.mapLabels f φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} (f : α → β) (X : Controlled T β R size gauge) (s t : T) (τ : HopfAlgebras.LRootedTree α) : (comapMapLabels f X).treeCoeff s t τ = X.treeCoeff s t (HopfAlgebras.LRootedTree.map f τ)

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapEraseLabels_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) : (comapEraseLabels X).toAlgebraic = AlgebraicLabelledBranchedRoughPath.comapEraseLabels X.toAlgebraic

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapConstLabel_toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (a : α) (X : Controlled T α R size gauge) : (comapConstLabel a X).toAlgebraic = AlgebraicLabelledBranchedRoughPath.comapConstLabel a X.toAlgebraic

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coeff_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) (s t : T) (φ : HopfAlgebras.LRootedForest α) : (comapEraseLabels X).coeff s t φ = X.coeff s t φ.erase

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) (s t : T) (τ : HopfAlgebras.LRootedTree α) : (comapEraseLabels X).treeCoeff s t τ = X.treeCoeff s t τ.erase

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coeff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (a : α) (X : Controlled T α R size gauge) (s t : T) (φ : HopfAlgebras.RootedForest) : (comapConstLabel a X).coeff s t φ = X.coeff s t (HopfAlgebras.LRootedForest.constLabel a φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (a : α) (X : Controlled T α R size gauge) (s t : T) (τ : HopfAlgebras.RootedTree) : (comapConstLabel a X).treeCoeff s t τ = X.treeCoeff s t (HopfAlgebras.LRootedTree.constLabel a τ)

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapTime_toAlgebraic {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 : Controlled T α R size gauge) : (comapTime f hf X).toAlgebraic = AlgebraicLabelledBranchedRoughPath.comapTime f X.toAlgebraic

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.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 : Controlled T α R size gauge) (s t : S) (φ : HopfAlgebras.LRootedForest α) : (comapTime f hf X).coeff s t φ = X.coeff (f s) (f t) φ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.treeCoeff_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 : Controlled T α R size gauge) (s t : S) (τ : HopfAlgebras.LRootedTree α) : (comapTime f hf X).treeCoeff s t τ = X.treeCoeff (f s) (f t) τ

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapMapLabels_id {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) : comapMapLabels id X = X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapMapLabels_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 : Controlled T γ R size gauge) : comapMapLabels f (comapMapLabels g X) = comapMapLabels (g ∘ f) X

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.comapConstLabel_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (a : α) (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) : comapConstLabel a (comapEraseLabels X) = X

def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.LabelInvariant {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) : Prop

A controlled labelled branched rough path whose algebraic part descends to unlabelled forests.

Equations

• X.LabelInvariant = X.toAlgebraic.LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.LabelInvariant.toAlgebraic {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X : Controlled T α R size gauge} (h : X.LabelInvariant) : X.toAlgebraic.LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.labelInvariant_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) : (comapEraseLabels X).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.LabelInvariant.comapMapLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {β : Type z} {X : Controlled T β R size gauge} (h : X.LabelInvariant) (f : α → β) : (Controlled.comapMapLabels f X).LabelInvariant

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.LabelInvariant.comapEraseLabels_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} {X : Controlled T α R size gauge} (h : X.LabelInvariant) (a : α) : comapEraseLabels (comapConstLabel a X) = X

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.labelInvariantEquiv {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} [Nonempty α] : AlgebraicBranchedRoughPath.Controlled T R size gauge ≃ { X : Controlled T α R size gauge // X.LabelInvariant }

Unlabelled controlled branched rough paths are equivalent to label-invariant labelled controlled branched rough paths.

Equations

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

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.labelInvariantEquiv_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} [Nonempty α] (X : AlgebraicBranchedRoughPath.Controlled T R size gauge) : ↑(labelInvariantEquiv X) = comapEraseLabels X

@[simp]

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.labelInvariantEquiv_symm_apply {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} [Nonempty α] (X : { X : Controlled T α R size gauge // X.LabelInvariant }) : labelInvariantEquiv.symm X = comapConstLabel (Classical.choice ⋯) ↑X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.labelInvariant_iff_exists_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} [Nonempty α] (X : Controlled T α R size gauge) : X.LabelInvariant ↔ ∃ (Y : AlgebraicBranchedRoughPath.Controlled T R size gauge), comapEraseLabels Y = X

@[simp]

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

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.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 : Controlled T α R size gauge) : comapTime g hg (comapTime f hf X) = comapTime (f ∘ g) ⋯ X

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.coordinate_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) {s t : T} (hst : s ≤ t) (φ : HopfAlgebras.LRootedForest α) : size (X.coeff s t φ) ≤ gauge φ.order (X.control.toFun s t)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.Controlled.tree_coordinate_bound {T : Type u} {α : Type v} {R : Type w} [Preorder T] [CommSemiring R] {size : R → ENNReal} {gauge : ℕ → ENNReal → ENNReal} (X : Controlled T α R size gauge) {s t : T} (hst : s ≤ t) (τ : HopfAlgebras.LRootedTree α) : size (X.treeCoeff s t τ) ≤ gauge τ.order (X.control.toFun s t)