1.31. ForMathlib.Probability.Kernel.Sigma
From the authors
Kernels on a sigma type
Kernel.sigma κ is the kernel on Σ a, β a which is κ a on the fiber β a.
Module LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma contains 5 exposed declarations.
-
ProbabilityTheory.Kernel.sigma -
ProbabilityTheory.Kernel.sigma_apply -
ProbabilityTheory.Kernel.sigma_apply_mk -
ProbabilityTheory.Kernel.comap_sigma_mk -
ProbabilityTheory.Kernel.instIsMarkovKernelSigmaSigma