Branched Log-Signatures

This file defines truncated convolution logarithms of rooted-forest characters. These are the Hopf-algebraic log-signatures associated with branched rough path increments.

@[reducible, inline]

abbrev RoughPaths.BranchedSignature (R : Type u) [CommSemiring R] : Type u

A branched signature is a character on the rooted-forest algebra.

Equations

• RoughPaths.BranchedSignature R = HopfAlgebras.ForestAlgebra.Character R

@[reducible, inline]

abbrev RoughPaths.LabelledBranchedSignature (α : Type u) (R : Type v) [CommSemiring R] : Type (max u v)

A labelled branched signature is a character on the labelled rooted-forest algebra.

Equations

• RoughPaths.LabelledBranchedSignature α R = HopfAlgebras.LForestAlgebra.Character α R

noncomputable def RoughPaths.BranchedSignature.logTruncated {R : Type u} [Field R] (χ : BranchedSignature R) (n : ℕ) : HopfAlgebras.ForestAlgebra.LinearFunctional R

The truncated branched log-signature of a forest character.

Equations

• χ.logTruncated n = HopfAlgebras.ForestAlgebra.LinearFunctional.logCharacterTruncated χ n

@[simp]

theorem RoughPaths.BranchedSignature.logTruncated_zero {R : Type u} [Field R] (χ : BranchedSignature R) : χ.logTruncated 0 = 0

@[simp]

theorem RoughPaths.BranchedSignature.logTruncated_unit {R : Type u} [Field R] (n : ℕ) : logTruncated (HopfAlgebras.ForestAlgebra.Character.unit R) n = 0

theorem RoughPaths.BranchedSignature.logTruncated_evalForest {R : Type u} [Field R] (χ : BranchedSignature R) (n : ℕ) (φ : HopfAlgebras.RootedForest) : (χ.logTruncated n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart χ).convolutionPower k).evalForest φ) (List.range n)).sum

theorem RoughPaths.BranchedSignature.logTruncated_evalTree {R : Type u} [Field R] (χ : BranchedSignature R) (n : ℕ) (τ : HopfAlgebras.RootedTree) : (χ.logTruncated n).evalForest (HopfAlgebras.RootedForest.singleton τ) = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart χ).convolutionPower k).evalForest (HopfAlgebras.RootedForest.singleton τ)) (List.range n)).sum

noncomputable def RoughPaths.LabelledBranchedSignature.logTruncated {α : Type u} {R : Type v} [Field R] (χ : LabelledBranchedSignature α R) (n : ℕ) : HopfAlgebras.LForestAlgebra.LinearFunctional α R

The truncated labelled branched log-signature of a labelled forest character.

Equations

• χ.logTruncated n = HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated χ n

@[simp]

theorem RoughPaths.LabelledBranchedSignature.logTruncated_zero {α : Type u} {R : Type v} [Field R] (χ : LabelledBranchedSignature α R) : χ.logTruncated 0 = 0

@[simp]

theorem RoughPaths.LabelledBranchedSignature.logTruncated_unit {α : Type u} {R : Type v} [Field R] (n : ℕ) : logTruncated (HopfAlgebras.LForestAlgebra.Character.unit α R) n = 0

theorem RoughPaths.LabelledBranchedSignature.logTruncated_evalForest {α : Type u} {R : Type v} [Field R] (χ : LabelledBranchedSignature α R) (n : ℕ) (φ : HopfAlgebras.LRootedForest α) : (χ.logTruncated n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart χ).convolutionPower k).evalForest φ) (List.range n)).sum

theorem RoughPaths.LabelledBranchedSignature.logTruncated_evalTree {α : Type u} {R : Type v} [Field R] (χ : LabelledBranchedSignature α R) (n : ℕ) (τ : HopfAlgebras.LRootedTree α) : (χ.logTruncated n).evalForest (HopfAlgebras.LRootedForest.singleton τ) = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart χ).convolutionPower k).evalForest (HopfAlgebras.LRootedForest.singleton τ)) (List.range n)).sum

theorem RoughPaths.LabelledBranchedSignature.logTruncated_comapMapLabels {α : Type u} {R : Type v} [Field R] {β : Type w} (f : α → β) (χ : LabelledBranchedSignature β R) (n : ℕ) : logTruncated (HopfAlgebras.LForestAlgebra.Character.comapMapLabels f χ) n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels f (χ.logTruncated n)

theorem RoughPaths.LabelledBranchedSignature.logTruncated_comapEraseLabels {α : Type u} {R : Type v} [Field R] (χ : BranchedSignature R) (n : ℕ) : logTruncated (HopfAlgebras.LForestAlgebra.Character.comapEraseLabels χ) n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels (χ.logTruncated n)

theorem RoughPaths.LabelledBranchedSignature.logTruncated_comapConstLabel {α : Type u} {R : Type v} [Field R] (a : α) (χ : LabelledBranchedSignature α R) (n : ℕ) : BranchedSignature.logTruncated (HopfAlgebras.LForestAlgebra.Character.comapConstLabel a χ) n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel a (χ.logTruncated n)

noncomputable def RoughPaths.AlgebraicBranchedRoughPath.logIncrementTruncated {T : Type u} {R : Type v} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) : HopfAlgebras.ForestAlgebra.LinearFunctional R

Truncated branched log-signature of a rough path increment.

Equations

• X.logIncrementTruncated s t n = RoughPaths.BranchedSignature.logTruncated (X.character s t) n

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.logIncrementTruncated_zero {T : Type u} {R : Type v} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) : X.logIncrementTruncated s t 0 = 0

@[simp]

theorem RoughPaths.AlgebraicBranchedRoughPath.logIncrementTruncated_self {T : Type u} {R : Type v} [Field R] (X : AlgebraicBranchedRoughPath T R) (t : T) (n : ℕ) : X.logIncrementTruncated t t n = 0

theorem RoughPaths.AlgebraicBranchedRoughPath.logIncrementTruncated_evalForest {T : Type u} {R : Type v} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) (φ : HopfAlgebras.RootedForest) : (X.logIncrementTruncated s t n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart (X.character s t)).convolutionPower k).evalForest φ) (List.range n)).sum

theorem RoughPaths.AlgebraicBranchedRoughPath.logIncrementTruncated_evalTree {T : Type u} {R : Type v} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) (τ : HopfAlgebras.RootedTree) : (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.RootedForest.singleton τ) = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart (X.character s t)).convolutionPower k).evalForest (HopfAlgebras.RootedForest.singleton τ)) (List.range n)).sum

theorem RoughPaths.AlgebraicBranchedRoughPath.AgreeUpToOrder.logIncrementTruncated {T : Type u} {R : Type v} [Field R] {X Y : AlgebraicBranchedRoughPath T R} {m n : ℕ} (h : X.AgreeUpToOrder Y n) (s t : T) : (X.logIncrementTruncated s t m).AgreeUpToOrder (Y.logIncrementTruncated s t m) n

theorem RoughPaths.AlgebraicBranchedRoughPath.AgreeUpToOrder.logIncrementTruncated_evalForest {T : Type u} {R : Type v} [Field R] {X Y : AlgebraicBranchedRoughPath T R} {m n : ℕ} (h : X.AgreeUpToOrder Y n) (s t : T) (φ : HopfAlgebras.RootedForest) (hφ : φ.order ≤ n) : (X.logIncrementTruncated s t m).evalForest φ = (Y.logIncrementTruncated s t m).evalForest φ

noncomputable def RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) : HopfAlgebras.LForestAlgebra.LinearFunctional α R

Truncated labelled branched log-signature of a rough path increment.

Equations

• X.logIncrementTruncated s t n = RoughPaths.LabelledBranchedSignature.logTruncated (X.lcharacter s t) n

@[simp]

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

@[simp]

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

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_evalForest {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) (φ : HopfAlgebras.LRootedForest α) : (X.logIncrementTruncated s t n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart (X.lcharacter s t)).convolutionPower k).evalForest φ) (List.range n)).sum

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_evalTree {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) (τ : HopfAlgebras.LRootedTree α) : (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.singleton τ) = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart (X.lcharacter s t)).convolutionPower k).evalForest (HopfAlgebras.LRootedForest.singleton τ)) (List.range n)).sum

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

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.AgreeUpToOrder.logIncrementTruncated_evalForest {T : Type u} {α : Type v} {R : Type w} [Field R] {X Y : AlgebraicLabelledBranchedRoughPath T α R} {m n : ℕ} (h : X.AgreeUpToOrder Y n) (s t : T) (φ : HopfAlgebras.LRootedForest α) (hφ : φ.order ≤ n) : (X.logIncrementTruncated s t m).evalForest φ = (Y.logIncrementTruncated s t m).evalForest φ

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapMapLabels {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) (n : ℕ) : (comapMapLabels f X).logIncrementTruncated s t n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels f (X.logIncrementTruncated s t n)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapMapLabels_evalForest {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) (n : ℕ) (φ : HopfAlgebras.LRootedForest α) : ((comapMapLabels f X).logIncrementTruncated s t n).evalForest φ = (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.mapLabels f φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapMapLabels_evalTree {T : Type u} {α : Type v} {R : Type w} [Field R] {β : Type z} (f : α → β) (X : AlgebraicLabelledBranchedRoughPath T β R) (s t : T) (n : ℕ) (τ : HopfAlgebras.LRootedTree α) : ((comapMapLabels f X).logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.singleton τ) = (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.singleton (HopfAlgebras.LRootedTree.map f τ))

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapEraseLabels {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) : (comapEraseLabels X).logIncrementTruncated s t n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels (X.logIncrementTruncated s t n)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapEraseLabels_evalForest {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) (φ : HopfAlgebras.LRootedForest α) : ((comapEraseLabels X).logIncrementTruncated s t n).evalForest φ = (X.logIncrementTruncated s t n).evalForest φ.erase

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapEraseLabels_evalTree {T : Type u} {α : Type v} {R : Type w} [Field R] (X : AlgebraicBranchedRoughPath T R) (s t : T) (n : ℕ) (τ : HopfAlgebras.LRootedTree α) : ((comapEraseLabels X).logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.singleton τ) = (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.RootedForest.singleton τ.erase)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapConstLabel {T : Type u} {α : Type v} {R : Type w} [Field R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) : (comapConstLabel a X).logIncrementTruncated s t n = HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel a (X.logIncrementTruncated s t n)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapConstLabel_evalForest {T : Type u} {α : Type v} {R : Type w} [Field R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) (φ : HopfAlgebras.RootedForest) : ((comapConstLabel a X).logIncrementTruncated s t n).evalForest φ = (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.constLabel a φ)

theorem RoughPaths.AlgebraicLabelledBranchedRoughPath.logIncrementTruncated_comapConstLabel_evalTree {T : Type u} {α : Type v} {R : Type w} [Field R] (a : α) (X : AlgebraicLabelledBranchedRoughPath T α R) (s t : T) (n : ℕ) (τ : HopfAlgebras.RootedTree) : ((comapConstLabel a X).logIncrementTruncated s t n).evalForest (HopfAlgebras.RootedForest.singleton τ) = (X.logIncrementTruncated s t n).evalForest (HopfAlgebras.LRootedForest.singleton (HopfAlgebras.LRootedTree.constLabel a τ))