Commit 2026-10-05 07:41 be31cde2

View on Github →

refactor(Probability/Distributions/Uniform): change uniformOfFinset and ofMultiset from PMF to Measure (#42909) Turn PMF.uniformOfFinset and PMF.ofMultiset into measures. This is part of #42821 which deprecates PMF.

Estimated changes

Modified Mathlib/Probability/Distributions/Uniform.lean

added def MeasureTheory.Measure.ofMultiset

added theorem MeasureTheory.Measure.ofMultiset_apply_singleton

added theorem MeasureTheory.Measure.ofMultiset_apply_singleton_of_notMem

added def MeasureTheory.Measure.uniformOfFinset

added theorem MeasureTheory.Measure.uniformOfFinset_apply

added theorem MeasureTheory.Measure.uniformOfFinset_apply_singleton

added theorem MeasureTheory.Measure.uniformOfFinset_apply_singleton_of_mem

added theorem MeasureTheory.Measure.uniformOfFinset_apply_singleton_of_notMem

deleted theorem PMF.mem_support_ofMultiset_iff

deleted theorem PMF.mem_support_uniformOfFinset_iff

deleted theorem PMF.mem_support_uniformOfFintype

deleted def PMF.ofMultiset

deleted theorem PMF.ofMultiset_apply

deleted theorem PMF.ofMultiset_apply_of_notMem

deleted theorem PMF.support_ofMultiset

deleted theorem PMF.support_uniformOfFinset

deleted theorem PMF.support_uniformOfFintype

deleted theorem PMF.toMeasure_ofMultiset_apply

deleted theorem PMF.toMeasure_uniformOfFinset_apply

deleted theorem PMF.toMeasure_uniformOfFintype_apply

deleted theorem PMF.toOuterMeasure_ofMultiset_apply

deleted theorem PMF.toOuterMeasure_uniformOfFinset_apply

deleted theorem PMF.toOuterMeasure_uniformOfFintype_apply

deleted def PMF.uniformOfFinset

deleted theorem PMF.uniformOfFinset_apply

deleted theorem PMF.uniformOfFinset_apply_of_mem

deleted theorem PMF.uniformOfFinset_apply_of_notMem

deleted def PMF.uniformOfFintype

deleted theorem PMF.uniformOfFintype_apply