Commit 2023-07-25 13:48 03720bd1

View on Github →

chore(Probability.Kernel): drop AEMeasurable assumptions (#6129)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

modified theorem MeasureTheory.Measure.fst_map_prod_mk

modified theorem MeasureTheory.Measure.fst_map_prod_mk₀

added theorem MeasureTheory.Measure.fst_zero

modified theorem MeasureTheory.Measure.snd_map_prod_mk

modified theorem MeasureTheory.Measure.snd_map_prod_mk₀

added theorem MeasureTheory.Measure.snd_zero

Modified Mathlib/Probability/Kernel/CondDistrib.lean

modified theorem MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_mk

modified theorem MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map

modified theorem MeasureTheory.Integrable.comp_snd_map_prod_mk

modified theorem MeasureTheory.Integrable.condDistrib_ae_map

modified theorem MeasureTheory.Integrable.integral_condDistrib_map

modified theorem MeasureTheory.Integrable.integral_norm_condDistrib_map

modified theorem MeasureTheory.Integrable.norm_integral_condDistrib_map