Signature kernels

The truncated signature kernel k_n(a, b) = Σ_{|w| ≤ n} a(w)·b(w) (Salvi, Cass, Foster, Lyons, Yang): symmetric, bilinear, and positive semidefinite — its Gram quadratic form is a sum of squares of feature evaluations. The word enumeration is parametrised by a listing of the alphabet, so it is computable: for piecewise-linear paths over ℚ concrete kernel values can be certified by native_decide.

def RoughPaths.Word.wordListOfLength {α : Type u} (letters : List α) : ℕ → List (List α)

All words of a given length over a listed alphabet.

Equations

• RoughPaths.Word.wordListOfLength letters 0 = [[]]
• RoughPaths.Word.wordListOfLength letters n.succ = List.flatMap (fun (a : α) => List.map (fun (w : List α) => a :: w) (RoughPaths.Word.wordListOfLength letters n)) letters

def RoughPaths.Word.kernelWords {α : Type u} (letters : List α) (n : ℕ) : List (List α)

All words of length at most n over a listed alphabet.

Equations

• RoughPaths.Word.kernelWords letters n = List.flatMap (RoughPaths.Word.wordListOfLength letters) (List.range (n + 1))

def RoughPaths.Word.sigKernelTruncated {α : Type u} {R : Type v} [CommSemiring R] (letters : List α) (a b : List α → R) (n : ℕ) : R

The truncated signature kernel: the ℓ²-pairing of word coefficients through length n, the alphabet being listed by letters.

Equations

• RoughPaths.Word.sigKernelTruncated letters a b n = (List.map (fun (w : List α) => RoughPaths.Word.coeff a w * RoughPaths.Word.coeff b w) (RoughPaths.Word.kernelWords letters n)).sum

theorem RoughPaths.Word.sigKernelTruncated_comm {α : Type u} {R : Type v} [CommSemiring R] (letters : List α) (a b : List α → R) (n : ℕ) : sigKernelTruncated letters a b n = sigKernelTruncated letters b a n

The kernel is symmetric.

theorem RoughPaths.Word.sigKernelTruncated_add_left {α : Type u} {R : Type v} [CommSemiring R] (letters : List α) (a a' b : List α → R) (n : ℕ) : sigKernelTruncated letters (a + a') b n = sigKernelTruncated letters a b n + sigKernelTruncated letters a' b n

The kernel is additive on the left (bilinearity).

theorem RoughPaths.Word.sigKernelTruncated_smul_left {α : Type u} {R : Type v} [CommSemiring R] (letters : List α) (r : R) (a b : List α → R) (n : ℕ) : sigKernelTruncated letters (r • a) b n = r * sigKernelTruncated letters a b n

The kernel scales on the left (bilinearity).

theorem RoughPaths.Word.sigKernelTruncated_quadratic_nonneg {α : Type u} {K : Type v} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] (letters : List α) {m : ℕ} (S : Fin m → List α → K) (c : Fin m → K) (n : ℕ) : 0 ≤ ∑ i : Fin m, ∑ j : Fin m, c i * c j * sigKernelTruncated letters (S i) (S j) n

Positive semidefiniteness of the truncated kernel: the Gram quadratic form is a sum of squares of feature evaluations.