Commit 2023-06-14 01:02 e6f9a50e

View on Github →

feat: port Probability.Kernel.MeasurableIntegral (#4884)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/MeasurableIntegral.lean

added theorem Measurable.lintegral_kernel

added theorem Measurable.lintegral_kernel_prod_left'

added theorem Measurable.lintegral_kernel_prod_left

added theorem Measurable.lintegral_kernel_prod_right''

added theorem Measurable.lintegral_kernel_prod_right'

added theorem Measurable.lintegral_kernel_prod_right

added theorem Measurable.set_lintegral_kernel

added theorem Measurable.set_lintegral_kernel_prod_left

added theorem Measurable.set_lintegral_kernel_prod_right

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left''

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_left

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right''

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'

added theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right

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

added theorem ProbabilityTheory.measurableSet_kernel_integrable