Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-10 11:38 3180fab6

View on Github →

feat(probability/kernel/composition): composition of kernels (#17974) We define the product, map, comap and composition of s-finite kernels.

Estimated changes

Created src/probability/kernel/composition.lean

added def probability_theory.kernel.comap

added theorem probability_theory.kernel.comap_apply'

added theorem probability_theory.kernel.comap_apply

added def probability_theory.kernel.comp

added theorem probability_theory.kernel.comp_apply

added theorem probability_theory.kernel.comp_assoc

added theorem probability_theory.kernel.comp_deterministic_eq_comap

added def probability_theory.kernel.comp_prod

added theorem probability_theory.kernel.comp_prod_apply

added theorem probability_theory.kernel.comp_prod_apply_eq_comp_prod_fun

added theorem probability_theory.kernel.comp_prod_apply_univ_le

added theorem probability_theory.kernel.comp_prod_eq_sum_comp_prod

added theorem probability_theory.kernel.comp_prod_eq_sum_comp_prod_left

added theorem probability_theory.kernel.comp_prod_eq_sum_comp_prod_right

added theorem probability_theory.kernel.comp_prod_eq_tsum_comp_prod

added def probability_theory.kernel.comp_prod_fun

added theorem probability_theory.kernel.comp_prod_fun_Union

added theorem probability_theory.kernel.comp_prod_fun_empty

added theorem probability_theory.kernel.comp_prod_fun_eq_tsum

added theorem probability_theory.kernel.comp_prod_fun_tsum_left

added theorem probability_theory.kernel.comp_prod_fun_tsum_right

added theorem probability_theory.kernel.deterministic_comp_eq_map

added def probability_theory.kernel.fst

added theorem probability_theory.kernel.fst_apply'

added theorem probability_theory.kernel.fst_apply

added theorem probability_theory.kernel.lintegral_comap

added theorem probability_theory.kernel.lintegral_comp

added theorem probability_theory.kernel.lintegral_comp_prod'

added theorem probability_theory.kernel.lintegral_comp_prod

added theorem probability_theory.kernel.lintegral_fst

added theorem probability_theory.kernel.lintegral_map

added theorem probability_theory.kernel.lintegral_prod

added theorem probability_theory.kernel.lintegral_prod_mk_left

added theorem probability_theory.kernel.lintegral_snd

added theorem probability_theory.kernel.lintegral_swap_left

added theorem probability_theory.kernel.lintegral_swap_right

added def probability_theory.kernel.map

added theorem probability_theory.kernel.map_apply'

added theorem probability_theory.kernel.map_apply

added theorem probability_theory.kernel.measurable_comp_prod_fun

added theorem probability_theory.kernel.measurable_comp_prod_fun_of_finite

added def probability_theory.kernel.prod

added theorem probability_theory.kernel.prod_apply

added def probability_theory.kernel.prod_mk_left

added theorem probability_theory.kernel.prod_mk_left_apply'

added theorem probability_theory.kernel.prod_mk_left_apply

added def probability_theory.kernel.snd

added theorem probability_theory.kernel.snd_apply'

added theorem probability_theory.kernel.snd_apply

added theorem probability_theory.kernel.sum_comap_seq

added theorem probability_theory.kernel.sum_map_seq

added def probability_theory.kernel.swap_left

added theorem probability_theory.kernel.swap_left_apply'

added theorem probability_theory.kernel.swap_left_apply

added def probability_theory.kernel.swap_right

added theorem probability_theory.kernel.swap_right_apply'

added theorem probability_theory.kernel.swap_right_apply