Commit 2023-05-22 03:13 14a08420

View on Github →

feat: port MeasureTheory.Measure.GiryMonad (#4103)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/GiryMonad.lean

added def MeasureTheory.Measure.bind

added theorem MeasureTheory.Measure.bind_apply

added theorem MeasureTheory.Measure.bind_bind

added theorem MeasureTheory.Measure.bind_dirac

added theorem MeasureTheory.Measure.bind_zero_left

added theorem MeasureTheory.Measure.bind_zero_right'

added theorem MeasureTheory.Measure.bind_zero_right

added theorem MeasureTheory.Measure.dirac_bind

added def MeasureTheory.Measure.join

added theorem MeasureTheory.Measure.join_apply

added theorem MeasureTheory.Measure.join_dirac

added theorem MeasureTheory.Measure.join_eq_bind

added theorem MeasureTheory.Measure.join_map_dirac

added theorem MeasureTheory.Measure.join_map_join

added theorem MeasureTheory.Measure.join_map_map

added theorem MeasureTheory.Measure.join_zero

added theorem MeasureTheory.Measure.lintegral_bind

added theorem MeasureTheory.Measure.lintegral_join

added theorem MeasureTheory.Measure.measurable_bind'

added theorem MeasureTheory.Measure.measurable_coe

added theorem MeasureTheory.Measure.measurable_dirac

added theorem MeasureTheory.Measure.measurable_join

added theorem MeasureTheory.Measure.measurable_lintegral

added theorem MeasureTheory.Measure.measurable_map

added theorem MeasureTheory.Measure.measurable_measure

added theorem MeasureTheory.Measure.measurable_of_measurable_coe