Commit 2023-05-26 15:03 7442e247

View on Github →

feat: port Probability.ProbabilityMassFunction.Constructions (#3928)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

added def Pmf.bernoulli

added theorem Pmf.bernoulli_apply

added theorem Pmf.bind_map

added theorem Pmf.bind_pure_comp

added def Pmf.filter

added theorem Pmf.filter_apply

added theorem Pmf.filter_apply_eq_zero_iff

added theorem Pmf.filter_apply_eq_zero_of_not_mem

added theorem Pmf.filter_apply_ne_zero_iff

added def Pmf.map

added theorem Pmf.map_apply

added theorem Pmf.map_bind

added theorem Pmf.map_comp

added theorem Pmf.map_const

added theorem Pmf.map_id

added theorem Pmf.mem_support_bernoulli_iff

added theorem Pmf.mem_support_filter_iff

added theorem Pmf.mem_support_map_iff

added theorem Pmf.mem_support_normalize_iff

added theorem Pmf.mem_support_ofFinset_iff

added theorem Pmf.mem_support_ofFintype_iff

added theorem Pmf.mem_support_seq_iff

added theorem Pmf.monad_map_eq_map

added theorem Pmf.monad_seq_eq_seq

added def Pmf.normalize

added theorem Pmf.normalize_apply

added def Pmf.ofFinset

added theorem Pmf.ofFinset_apply

added theorem Pmf.ofFinset_apply_of_not_mem

added def Pmf.ofFintype

added theorem Pmf.ofFintype_apply

added theorem Pmf.pure_map

added def Pmf.seq

added theorem Pmf.seq_apply

added theorem Pmf.support_bernoulli

added theorem Pmf.support_filter

added theorem Pmf.support_map

added theorem Pmf.support_normalize

added theorem Pmf.support_ofFinset

added theorem Pmf.support_ofFintype

added theorem Pmf.support_seq

added theorem Pmf.toMeasure_map_apply

added theorem Pmf.toMeasure_ofFinset_apply

added theorem Pmf.toMeasure_ofFintype_apply

added theorem Pmf.toOuterMeasure_map_apply

added theorem Pmf.toOuterMeasure_ofFinset_apply

added theorem Pmf.toOuterMeasure_ofFintype_apply