Commit 2023-05-22 10:23 3b88f400

View on Github →

feat(probability/kernel/disintegration): disintegration of finite measures on product spaces (#18834) Disintegration of finite measures on α × Ω, where Ω is a standard Borel space.

Estimated changes

Modified src/measure_theory/constructions/prod/basic.lean

added theorem measurable_embedding.prod_mk

Modified src/probability/kernel/cond_cdf.lean

added theorem probability_theory.measurable_measure_cond_cdf

added theorem probability_theory.measure_cond_cdf_Iic

added theorem probability_theory.measure_cond_cdf_univ

Created src/probability/kernel/disintegration.lean

added def measure_theory.measure.cond_kernel

added theorem probability_theory.ae_cond_kernel_real_eq_one

added theorem probability_theory.cond_kernel_def

added def probability_theory.cond_kernel_real

added theorem probability_theory.cond_kernel_real_Iic

added theorem probability_theory.exists_cond_kernel

added theorem probability_theory.kernel.const_eq_comp_prod

added theorem probability_theory.kernel.const_eq_comp_prod_real

added theorem probability_theory.kernel.const_unit_eq_comp_prod

added theorem probability_theory.lintegral_cond_kernel

added theorem probability_theory.lintegral_cond_kernel_mem

added theorem probability_theory.lintegral_cond_kernel_real

added theorem probability_theory.lintegral_cond_kernel_real_mem

added theorem probability_theory.lintegral_cond_kernel_real_univ

added theorem probability_theory.measure_eq_comp_prod

added theorem probability_theory.measure_eq_comp_prod_real

added theorem probability_theory.set_lintegral_cond_kernel_real_Iic

added theorem probability_theory.set_lintegral_cond_kernel_real_prod

added theorem probability_theory.set_lintegral_cond_kernel_real_univ