Commit 2023-06-16 12:59 a5204f8c

View on Github →

feat: port Probability.Kernel.Composition (#5044)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.kernel.ae_ae_of_ae_compProd

added theorem ProbabilityTheory.kernel.ae_kernel_lt_top

added theorem ProbabilityTheory.kernel.ae_null_of_compProd_null

added def ProbabilityTheory.kernel.comap

added theorem ProbabilityTheory.kernel.comap_apply'

added theorem ProbabilityTheory.kernel.comap_apply

added theorem ProbabilityTheory.kernel.compProdFun_empty

added theorem ProbabilityTheory.kernel.compProdFun_eq_tsum

added theorem ProbabilityTheory.kernel.compProdFun_iUnion

added theorem ProbabilityTheory.kernel.compProdFun_tsum_left

added theorem ProbabilityTheory.kernel.compProdFun_tsum_right

added theorem ProbabilityTheory.kernel.compProd_apply

added theorem ProbabilityTheory.kernel.compProd_apply_eq_compProdFun

added theorem ProbabilityTheory.kernel.compProd_apply_univ_le

added theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd

added theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_left

added theorem ProbabilityTheory.kernel.compProd_eq_sum_compProd_right

added theorem ProbabilityTheory.kernel.compProd_eq_tsum_compProd

added theorem ProbabilityTheory.kernel.compProd_null

added theorem ProbabilityTheory.kernel.compProd_restrict

added theorem ProbabilityTheory.kernel.compProd_restrict_left

added theorem ProbabilityTheory.kernel.compProd_restrict_right

added theorem ProbabilityTheory.kernel.comp_apply'

added theorem ProbabilityTheory.kernel.comp_apply

added theorem ProbabilityTheory.kernel.comp_assoc

added theorem ProbabilityTheory.kernel.comp_deterministic_eq_comap

added theorem ProbabilityTheory.kernel.comp_eq_snd_compProd

added theorem ProbabilityTheory.kernel.deterministic_comp_eq_map

added theorem ProbabilityTheory.kernel.fst_apply'

added theorem ProbabilityTheory.kernel.fst_apply

added theorem ProbabilityTheory.kernel.le_compProd_apply

added theorem ProbabilityTheory.kernel.lintegral_comap

added theorem ProbabilityTheory.kernel.lintegral_comp

added theorem ProbabilityTheory.kernel.lintegral_compProd'

added theorem ProbabilityTheory.kernel.lintegral_compProd

added theorem ProbabilityTheory.kernel.lintegral_compProd₀

added theorem ProbabilityTheory.kernel.lintegral_fst

added theorem ProbabilityTheory.kernel.lintegral_prod

added theorem ProbabilityTheory.kernel.lintegral_prodMkLeft

added theorem ProbabilityTheory.kernel.lintegral_snd

added theorem ProbabilityTheory.kernel.lintegral_swapLeft

added theorem ProbabilityTheory.kernel.lintegral_swapRight

added theorem ProbabilityTheory.kernel.map_apply'

added theorem ProbabilityTheory.kernel.map_apply

added theorem ProbabilityTheory.kernel.measurable_compProdFun

added theorem ProbabilityTheory.kernel.measurable_compProdFun_of_finite

added def ProbabilityTheory.kernel.prodMkLeft

added theorem ProbabilityTheory.kernel.prodMkLeft_apply'

added theorem ProbabilityTheory.kernel.prodMkLeft_apply

added theorem ProbabilityTheory.kernel.prod_apply

added theorem ProbabilityTheory.kernel.set_lintegral_compProd

added theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_left

added theorem ProbabilityTheory.kernel.set_lintegral_compProd_univ_right

added theorem ProbabilityTheory.kernel.snd_apply'

added theorem ProbabilityTheory.kernel.snd_apply

added theorem ProbabilityTheory.kernel.sum_comap_seq

added theorem ProbabilityTheory.kernel.sum_map_seq

added def ProbabilityTheory.kernel.swapLeft

added theorem ProbabilityTheory.kernel.swapLeft_apply'

added theorem ProbabilityTheory.kernel.swapLeft_apply

added theorem ProbabilityTheory.kernel.swapRight_apply'

added theorem ProbabilityTheory.kernel.swapRight_apply

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left'

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_left_of_finite

deleted theorem ProbabilityTheory.Kernel.measurable_kernel_prod_mk_right

deleted theorem ProbabilityTheory.Kernel.measurable_lintegral_indicator_const

added theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left'

added theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left

added theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite

added theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_right

added theorem ProbabilityTheory.kernel.measurable_lintegral_indicator_const