Commit 2024-08-29 06:53 4fd26e9a

View on Github →

feat: add a new class IsZeroOrProbabilityMeasure (#16130) The need for this class has shown up in PFR: when conditioning on a set, one gets a measure which is either zero or a probability measure, and many results that hold for probability measures also hold trivially for the zero measure.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.comap_zero

modified theorem MeasureTheory.OuterMeasure.toMeasure_zero

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.eq_zero_or_isProbabilityMeasure

added theorem MeasureTheory.isZeroOrProbabilityMeasure_iff

modified theorem MeasureTheory.one_le_prob_iff

modified theorem MeasureTheory.prob_le_one

Modified Mathlib/Probability/CDF.lean

Modified Mathlib/Probability/CondCount.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Independence/ZeroOne.lean

Modified Mathlib/Probability/Moments.lean

modified theorem ProbabilityTheory.centralMoment_one

modified theorem ProbabilityTheory.cgf_zero

modified theorem ProbabilityTheory.iIndepFun.cgf_sum

modified theorem ProbabilityTheory.iIndepFun.integrable_exp_mul_sum

modified theorem ProbabilityTheory.iIndepFun.mgf_sum

Modified scripts/style-exceptions.txt