Commit 2023-05-09 10:06 68b21e12

View on Github →

feat: port Probability.ProbabilityMassFunction.Basic (#3865)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ProbabilityMassFunction/Basic.lean

added def MeasureTheory.Measure.toPmf

added theorem MeasureTheory.Measure.toPmf_apply

added theorem MeasureTheory.Measure.toPmf_toMeasure

added theorem Pmf.apply_eq_one_iff

added theorem Pmf.apply_eq_zero_iff

added theorem Pmf.apply_lt_top

added theorem Pmf.apply_ne_top

added theorem Pmf.apply_pos_iff

added theorem Pmf.coe_le_one

added theorem Pmf.coe_ne_zero

added theorem Pmf.ext_iff

added theorem Pmf.hasSum_coe_one

added theorem Pmf.mem_support_iff

added def Pmf.support

added theorem Pmf.support_nonempty

added def Pmf.toMeasure

added theorem Pmf.toMeasure_apply

added theorem Pmf.toMeasure_apply_eq_of_inter_support_eq

added theorem Pmf.toMeasure_apply_eq_one_iff

added theorem Pmf.toMeasure_apply_eq_toOuterMeasure_apply

added theorem Pmf.toMeasure_apply_eq_zero_iff

added theorem Pmf.toMeasure_apply_finset

added theorem Pmf.toMeasure_apply_fintype

added theorem Pmf.toMeasure_apply_inter_support

added theorem Pmf.toMeasure_apply_of_finite

added theorem Pmf.toMeasure_apply_singleton

added theorem Pmf.toMeasure_eq_iff_eq_toPmf

added theorem Pmf.toMeasure_inj

added theorem Pmf.toMeasure_injective

added theorem Pmf.toMeasure_mono

added theorem Pmf.toMeasure_toPmf

added def Pmf.toOuterMeasure

added theorem Pmf.toOuterMeasure_apply

added theorem Pmf.toOuterMeasure_apply_eq_of_inter_support_eq

added theorem Pmf.toOuterMeasure_apply_eq_one_iff

added theorem Pmf.toOuterMeasure_apply_eq_zero_iff

added theorem Pmf.toOuterMeasure_apply_finset

added theorem Pmf.toOuterMeasure_apply_fintype

added theorem Pmf.toOuterMeasure_apply_inter_support

added theorem Pmf.toOuterMeasure_apply_le_toMeasure_apply

added theorem Pmf.toOuterMeasure_apply_singleton

added theorem Pmf.toOuterMeasure_caratheodory

added theorem Pmf.toOuterMeasure_inj

added theorem Pmf.toOuterMeasure_injective

added theorem Pmf.toOuterMeasure_mono

added theorem Pmf.toPmf_eq_iff_toMeasure_eq

added theorem Pmf.tsum_coe

added theorem Pmf.tsum_coe_indicator_ne_top

added theorem Pmf.tsum_coe_ne_top

added def Pmf.{u}