Commit 2024-12-12 18:01 fdbd2e1a

View on Github →

feat(GiryMonad): add Measurable.measure_of_isPiSystem (#19908) ... and use it to golf some Measurable (_ : _ → Measure _) theorems.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

added theorem Measurable.measure_of_isPiSystem

added theorem Measurable.measure_of_isPiSystem_of_isProbabilityMeasure

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

deleted theorem ProbabilityTheory.StieltjesFunction.measurable_measure

Modified Mathlib/Probability/Kernel/Disintegration/CondCDF.lean

Modified Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean

added theorem StieltjesFunction.measurable_measure