1.3. ForMathlib.Probability.Kernel.Composition.MapComap
Lemmas about map and comap of Markov kernels
Module LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap contains 5 exposed declarations.
-
ProbabilityTheory.Kernel.prodMkLeft_inj -
ProbabilityTheory.Kernel.prodMkRight_inj -
ProbabilityTheory.Kernel.prodMkLeft_deterministic -
ProbabilityTheory.Kernel.prodMkRight_deterministic -
ProbabilityTheory.Kernel.comap_const