1.1. Usage🔗

To use Kernel-Hom, add the following to your lakefile.toml:

[[require]]
name = "kernelhom"
git = "https://github.com/gaetanserre/KernelHom.git"

or to your lakefile.lean:

require kernelhom from git "https://github.com/gaetanserre/KernelHom" @ "main"

Then, in your Lean files, you can import the library with:

import KernelHom

Tactics

The library provides several tactics for working with s-finite kernels equalities. The main tactics are:

• kernel_hom: Transforms a s-finite kernel equality into an equality in the SFinKer monoidal category.

• hom_kernel: The inverse of kernel_hom, transforms an equality in SFinKer back into a kernel equality.

• kernel_disch: The tactic to use by default. Applies the cat_disch and monoidal tactics to a s-finite kernel equality, possibly after normalizing the tensor products of morphisms, so that it also handles the exchange law and the comonoid laws of copy and discard.

• kernel_monoidal: Applies the monoidal tactic to a s-finite kernel equality.

• kernel_coherence: Applies the coherence tactic to a s-finite kernel equality.

• aesop_kernel: Applies aesop with the CategoryTheory rule set to a s-finite kernel equality, without the rfl_cat attempt of cat_disch.

Basically, whenever you have a equality of s-finite kernels that you want to simplify, you can apply kernel_hom to transform it into a categorical equality, try applying categorical tactics, simps, or manually manipulate it, and then apply hom_kernel to get back to a kernel equality if needed. The built-in helpers kernel_disch, kernel_monoidal, kernel_coherence and aesop_kernel directly apply categorical tactics to kernels without needing to manually invoke the translation tactic.

Kernel diagrams

The library also provides the kernel_diagram command, which generates string diagrams for kernel expressions. This is an adaptation of the string_diagram command, where s-finite kernels are represented as morphisms using kernel_hom. This provides a visual representation of kernel compositions and transformations, aiding intuition and understanding. The use of this command is similar to string_diagram:

1.2. Examples🔗

Kernel-Hom makes it easy to prove "API" lemmas about the usual operations on kernels. The following lemmas of Mathlib are equalities of kernels built only from composition, parallel composition, product, identity, copy and swap. In Mathlib, their proofs either manipulate integrals or rely on other lemmas about kernels. With Kernel-Hom, they are proved from the structure of SFinKer, without any knowledge of the lemmas about kernels. They are collected in the file KernelHomTests/Examples.lean, where their names are suffixed by ₀. The tactics are also useful in longer proofs, written by calculation (see the calculational proof of Basu's theorem).

The other lemmas of Mathlib built from these operations, such as comp_assoc, swap_parallelComp or parallelComp_comp_parallelComp, are used, directly or not, to prove the axioms of SFinKer. The tactics also prove them, but these proofs could not replace the ones of Mathlib, so they are not listed here.

As Kernel.map is not translated, map_prod_swap and prodAssoc_prod are first rewritten with swap_comp_eq_map and deterministic_comp_eq_map. The tactics only apply to s-finite kernels: as in Mathlib, the case of a non s-finite kernel in parallelComp_comm is closed by simp.

All of them are proved by a single call to kernel_disch or kernel_monoidal. In particular, kernel_disch handles the exchange law whisker_exchange in parallelComp_comm, and the coassociativity of copy comul_assoc in prodAssoc_prod, which the tactics of Mathlib do not apply on their own.

Mathlib.Probability.Kernel.Composition.Prod

The kernel Kernel.swap is translated to the braiding of SFinKer, and the product κ ×ₖ η to the composition of the copy with κ ⊗ₘ η.

Mathlib.Probability.Kernel.Composition.KernelLemmas

The diagram below is drawn for s-finite kernels.