Commit 2023-06-01 15:15 b0cc020d

View on Github →

feat: port Probability.ProbabilityMassFunction.Uniform (#4463) Please feel free to push to this branch. One proof remaining:

toOuterMeasure_uniformOfFintype_apply

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ProbabilityMassFunction/Uniform.lean

added theorem Pmf.mem_support_ofMultiset_iff

added theorem Pmf.mem_support_uniformOfFinset_iff

added theorem Pmf.mem_support_uniformOfFintype

added def Pmf.ofMultiset

added theorem Pmf.ofMultiset_apply

added theorem Pmf.ofMultiset_apply_of_not_mem

added theorem Pmf.support_ofMultiset

added theorem Pmf.support_uniformOfFinset

added theorem Pmf.support_uniformOfFintype

added theorem Pmf.toMeasure_ofMultiset_apply

added theorem Pmf.toMeasure_uniformOfFinset_apply

added theorem Pmf.toMeasure_uniformOfFintype_apply

added theorem Pmf.toOuterMeasure_ofMultiset_apply

added theorem Pmf.toOuterMeasure_uniformOfFinset_apply

added theorem Pmf.toOuterMeasure_uniformOfFintype_apply

added def Pmf.uniformOfFinset

added theorem Pmf.uniformOfFinset_apply

added theorem Pmf.uniformOfFinset_apply_of_mem

added theorem Pmf.uniformOfFinset_apply_of_not_mem

added def Pmf.uniformOfFintype

added theorem Pmf.uniformOfFintype_apply