Commit 2024-01-16 19:40 e8248a26

View on Github →

feat(Probability): simple kernel lemmas (#9350)

Lemmas about compositions and products of kernels.
New definition: prodMkRight, similar to prodMkLeft: takes κ : kernel α β and turn it into a kernel (α × γ) β. From the PFR project.

Estimated changes

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.comap_map_comm

added theorem ProbabilityTheory.kernel.fst_prod

added theorem ProbabilityTheory.kernel.fst_prodMkLeft

added theorem ProbabilityTheory.kernel.fst_prodMkRight

added theorem ProbabilityTheory.kernel.lintegral_prodMkRight

added theorem ProbabilityTheory.kernel.map_prodMkLeft

added theorem ProbabilityTheory.kernel.map_prodMkRight

added def ProbabilityTheory.kernel.prodMkRight

added theorem ProbabilityTheory.kernel.prodMkRight_apply'

added theorem ProbabilityTheory.kernel.prodMkRight_apply

added theorem ProbabilityTheory.kernel.prodMkRight_zero

added theorem ProbabilityTheory.kernel.prod_apply'

modified theorem ProbabilityTheory.kernel.prod_apply

added theorem ProbabilityTheory.kernel.prod_const

added theorem ProbabilityTheory.kernel.snd_prod

added theorem ProbabilityTheory.kernel.snd_prodMkLeft

added theorem ProbabilityTheory.kernel.snd_prodMkRight

added theorem ProbabilityTheory.kernel.swapLeft_prodMkLeft

added theorem ProbabilityTheory.kernel.swapLeft_prodMkRight