Commit 2023-12-26 19:32 e62554d2

View on Github →

feat: Basic probability lemmas assuming null-measurability (#9222) and transferring probabiity measures across ULift From LeanCamCombi and PFR

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

modified theorem MeasureTheory.isProbabilityMeasure_map

added theorem MeasureTheory.mem_ae_iff_prob_eq_one₀

modified theorem MeasureTheory.one_le_prob_iff

modified theorem MeasureTheory.prob_compl_eq_one_iff

added theorem MeasureTheory.prob_compl_eq_one_iff₀

modified theorem MeasureTheory.prob_compl_eq_one_sub

added theorem MeasureTheory.prob_compl_eq_one_sub₀

modified theorem MeasureTheory.prob_compl_eq_zero_iff

added theorem MeasureTheory.prob_compl_eq_zero_iff₀