Commit 2023-11-21 07:51 7d85f2f4

View on Github →

feat(Probability): add simp lemmas for kernels (#8497)

Estimated changes

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.kernel.const_zero

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.fst_compProd

added theorem ProbabilityTheory.kernel.fst_map_prod

added theorem ProbabilityTheory.kernel.fst_swapRight

added theorem ProbabilityTheory.kernel.fst_zero

added theorem ProbabilityTheory.kernel.map_const

added theorem ProbabilityTheory.kernel.prodMkLeft_zero

added theorem ProbabilityTheory.kernel.snd_map_prod

added theorem ProbabilityTheory.kernel.snd_swapRight

added theorem ProbabilityTheory.kernel.snd_zero

modified theorem ProbabilityTheory.kernel.swapLeft_apply