LeanMachineLearning

4.20. Tactic.KernelHom.Tactic.KernelDiagram🔗

Kernel Diagram Widget

This file provides meta infrastructure for displaying string diagrams for s-finite kernels in the infoview. To enable the kernel diagram widget, you need to import this file and inserting with_panel_widgets [KernelDiagram] at the beginning of the proof. Alternatively, you can also write

show_panel_widgets [local KernelDiagram]

to enable the string diagram widget in the current section.

We also have the #kernel_diagram command. For example,

#string_diagram ProbabilityTheory.Kernel.deterministic_comp_copy

This is an adaptation of the string diagram widget where kernels are transformed into morphisms of the SFinKer monoidal category using the kernel_hom tactic.

Module LeanMachineLearning.Tactic.KernelHom.Tactic.KernelDiagram contains 10 exposed declarations.