Commit 2023-06-21 05:19 c330e8c1

View on Github →

feat: port Probability.Kernel.Condexp (#5324)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/Condexp.lean

added theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id

added theorem MeasureTheory.AEStronglyMeasurable.integral_condexpKernel

added theorem MeasureTheory.Integrable.comp_snd_map_prod_id

added theorem MeasureTheory.Integrable.condexpKernel_ae

added theorem MeasureTheory.Integrable.integral_condexpKernel

added theorem MeasureTheory.Integrable.integral_norm_condexpKernel

added theorem MeasureTheory.Integrable.norm_integral_condexpKernel

added theorem ProbabilityTheory.aemeasurable_id''

added theorem ProbabilityTheory.aestronglyMeasurable'_integral_condexpKernel

added theorem ProbabilityTheory.condexp_ae_eq_integral_condexpKernel

added theorem ProbabilityTheory.integrable_toReal_condexpKernel

added theorem ProbabilityTheory.measurable_condexpKernel

added theorem ProbabilityTheory.measurable_id''