Commit 2023-05-24 11:30 6315581f

View on Github →

feat(probability/kernel/disintegration): integral against cond_kernel (#19066)

Estimated changes

Modified src/probability/kernel/disintegration.lean

added theorem measure_theory.ae_strongly_measurable.ae_integrable_cond_kernel_iff

added theorem measure_theory.ae_strongly_measurable.integral_cond_kernel

added theorem measure_theory.integrable.cond_kernel_ae

added theorem measure_theory.integrable.integral_cond_kernel

added theorem measure_theory.integrable.integral_norm_cond_kernel

added theorem measure_theory.integrable.norm_integral_cond_kernel

added theorem probability_theory.integral_cond_kernel

added theorem probability_theory.set_integral_cond_kernel

added theorem probability_theory.set_integral_cond_kernel_univ_left

added theorem probability_theory.set_integral_cond_kernel_univ_right

added theorem probability_theory.set_lintegral_cond_kernel

added theorem probability_theory.set_lintegral_cond_kernel_eq_measure_prod

added theorem probability_theory.set_lintegral_cond_kernel_univ_left

added theorem probability_theory.set_lintegral_cond_kernel_univ_right