Commit 2024-10-12 06:38 3f143f7d

View on Github →

feat(Probability/Kernel): simple lemmas about composition of kernels (#17596)

Estimated changes

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.Kernel.comp_zero

added theorem ProbabilityTheory.Kernel.deterministic_comp_deterministic

added theorem ProbabilityTheory.Kernel.deterministic_prod_deterministic

added theorem ProbabilityTheory.Kernel.fst_comp

added theorem ProbabilityTheory.Kernel.map_comp

added theorem ProbabilityTheory.Kernel.snd_comp

added theorem ProbabilityTheory.Kernel.snd_compProd_prodMkLeft

added theorem ProbabilityTheory.Kernel.zero_comp