Mathlib Changelog
Changelog
About
Github
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