Commit 2023-06-20 11:06 88b496d8

View on Github →

feat: port Probability.Kernel.Disintegration (#5289)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Probability/Kernel/CondCdf.lean

Created Mathlib/Probability/Kernel/Disintegration.lean

added theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff

added theorem MeasureTheory.AEStronglyMeasurable.integral_condKernel

added theorem MeasureTheory.Integrable.condKernel_ae

added theorem MeasureTheory.Integrable.integral_condKernel

added theorem MeasureTheory.Integrable.integral_norm_condKernel

added theorem MeasureTheory.Integrable.norm_integral_condKernel

added theorem ProbabilityTheory.ae_condKernelReal_eq_one

added theorem ProbabilityTheory.condKernelReal_Iic

added theorem ProbabilityTheory.condKernel_def

added theorem ProbabilityTheory.exists_cond_kernel

added theorem ProbabilityTheory.integral_condKernel

added theorem ProbabilityTheory.kernel.const_eq_compProd

added theorem ProbabilityTheory.kernel.const_eq_compProd_real

added theorem ProbabilityTheory.kernel.const_unit_eq_compProd

added theorem ProbabilityTheory.lintegral_condKernel

added theorem ProbabilityTheory.lintegral_condKernelReal

added theorem ProbabilityTheory.lintegral_condKernelReal_mem

added theorem ProbabilityTheory.lintegral_condKernelReal_univ

added theorem ProbabilityTheory.lintegral_condKernel_mem

added theorem ProbabilityTheory.measure_eq_compProd

added theorem ProbabilityTheory.measure_eq_compProd_real

added theorem ProbabilityTheory.set_integral_condKernel

added theorem ProbabilityTheory.set_integral_condKernel_univ_left

added theorem ProbabilityTheory.set_integral_condKernel_univ_right

added theorem ProbabilityTheory.set_lintegral_condKernel

added theorem ProbabilityTheory.set_lintegral_condKernelReal_Iic

added theorem ProbabilityTheory.set_lintegral_condKernelReal_prod

added theorem ProbabilityTheory.set_lintegral_condKernelReal_univ

added theorem ProbabilityTheory.set_lintegral_condKernel_eq_measure_prod

added theorem ProbabilityTheory.set_lintegral_condKernel_univ_left

added theorem ProbabilityTheory.set_lintegral_condKernel_univ_right