Mathlib Changelog
v4
Changelog
About
Github
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