4.14. Tactic.KernelHom.Kernel.MonoidalComp
Measurable coherence
This file introduces the monoidal composition for s-finite kernels (noted ⊗≫ₖ).
Main declarations
-
MeasurableCoherence: class witnessing measurable equivalences between types. -
monoComp: monoidal composition of kernels using measurable equivalences to transport toSFinKer. -
hom_monoComp: theSFinKermorphism of the kernelized monoidal composition is the monoidal composition of the morphisms inSFinKer.
Module LeanMachineLearning.Tactic.KernelHom.Kernel.MonoidalComp contains 8 exposed declarations.
-
MeasurableCoherence -
MeasurableCoherence.inst -
MeasurableCoherence.TransEquiv -
MeasurableCoherence.monoidalCoherence -
ProbabilityTheory.Kernel.monoComp₀ -
ProbabilityTheory.Kernel.monoComp'_sfinite -
ProbabilityTheory.Kernel.monoComp -
ProbabilityTheory.«term_⊗≫ₖ_»