Commit 2024-11-28 16:12 a906a97e

View on Github →

feat(Probability): identity, copy, discard and swap kernels (#19481) Add some notable deterministic kernels. These kernels play a particular role in the Markov category point of view on probability transition kernels. From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/Probability/Kernel/Basic.lean

added def ProbabilityTheory.Kernel.copy

added theorem ProbabilityTheory.Kernel.copy_apply

added def ProbabilityTheory.Kernel.discard

added theorem ProbabilityTheory.Kernel.discard_apply

added def ProbabilityTheory.Kernel.id

added theorem ProbabilityTheory.Kernel.id_apply

added def ProbabilityTheory.Kernel.swap

added theorem ProbabilityTheory.Kernel.swap_apply'

added theorem ProbabilityTheory.Kernel.swap_apply

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp

added theorem ProbabilityTheory.Kernel.comp_discard

added theorem ProbabilityTheory.Kernel.comp_id

added theorem ProbabilityTheory.Kernel.id_comp

added theorem ProbabilityTheory.Kernel.swap_comp_eq_map

added theorem ProbabilityTheory.Kernel.swap_copy

added theorem ProbabilityTheory.Kernel.swap_prod

added theorem ProbabilityTheory.Kernel.swap_swap