Commit 2023-06-21 00:53 b8eff30e

View on Github →

feat: port Probability.Kernel.CondDistrib (#5293)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Kernel/CondDistrib.lean

added theorem MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff

added theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk

added theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib

added theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map

added theorem MeasureTheory.Integrable.comp_snd_map_prod_mk

added theorem MeasureTheory.Integrable.condDistrib_ae

added theorem MeasureTheory.Integrable.condDistrib_ae_map

added theorem MeasureTheory.Integrable.integral_condDistrib

added theorem MeasureTheory.Integrable.integral_condDistrib_map

added theorem MeasureTheory.Integrable.integral_norm_condDistrib

added theorem MeasureTheory.Integrable.integral_norm_condDistrib_map

added theorem MeasureTheory.Integrable.norm_integral_condDistrib

added theorem MeasureTheory.Integrable.norm_integral_condDistrib_map

added theorem ProbabilityTheory.aestronglyMeasurable'_integral_condDistrib

added theorem ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prod_mk_iff

added theorem ProbabilityTheory.condDistrib_ae_eq_condexp

added theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib'

added theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib

added theorem ProbabilityTheory.condexp_ae_eq_integral_condDistrib_id

added theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib'

added theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib

added theorem ProbabilityTheory.condexp_prod_ae_eq_integral_condDistrib₀

added theorem ProbabilityTheory.integrable_comp_snd_map_prod_mk_iff

added theorem ProbabilityTheory.integrable_toReal_condDistrib

added theorem ProbabilityTheory.measurable_condDistrib

added theorem ProbabilityTheory.set_lintegral_condDistrib_of_measurableSet

added theorem ProbabilityTheory.set_lintegral_preimage_condDistrib