Commit 2023-10-06 14:17 2dac27d7

View on Github →

chore(Probability): rename Pmf to PMF (#7542) Search and replace Pmf with PMF.

Estimated changes

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_countable
added theorem PMF.support_nonempty
added def PMF.toMeasure
added theorem PMF.toMeasure_apply
added theorem PMF.toMeasure_inj
added theorem PMF.toMeasure_mono
added theorem PMF.toMeasure_toPMF
added theorem PMF.toOuterMeasure_inj
added theorem PMF.tsum_coe
added theorem PMF.tsum_coe_ne_top
added def PMF.{u}
deleted theorem Pmf.apply_eq_one_iff
deleted theorem Pmf.apply_eq_zero_iff
deleted theorem Pmf.apply_lt_top
deleted theorem Pmf.apply_ne_top
deleted theorem Pmf.apply_pos_iff
deleted theorem Pmf.coe_le_one
deleted theorem Pmf.coe_ne_zero
deleted theorem Pmf.ext_iff
deleted theorem Pmf.hasSum_coe_one
deleted theorem Pmf.mem_support_iff
deleted def Pmf.support
deleted theorem Pmf.support_countable
deleted theorem Pmf.support_nonempty
deleted def Pmf.toMeasure
deleted theorem Pmf.toMeasure_apply
deleted theorem Pmf.toMeasure_inj
deleted theorem Pmf.toMeasure_injective
deleted theorem Pmf.toMeasure_mono
deleted theorem Pmf.toMeasure_toPmf
deleted def Pmf.toOuterMeasure
deleted theorem Pmf.toOuterMeasure_apply
deleted theorem Pmf.toOuterMeasure_inj
deleted theorem Pmf.toOuterMeasure_mono
deleted theorem Pmf.tsum_coe
deleted theorem Pmf.tsum_coe_ne_top
deleted def Pmf.{u}
added def PMF.binomial
added theorem PMF.binomial_apply
deleted def Pmf.binomial
deleted theorem Pmf.binomial_apply
deleted theorem Pmf.binomial_apply_self
deleted theorem Pmf.binomial_apply_zero
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 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.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 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
deleted def Pmf.bernoulli
deleted theorem Pmf.bernoulli_apply
deleted theorem Pmf.bind_map
deleted theorem Pmf.bind_pure_comp
deleted def Pmf.filter
deleted theorem Pmf.filter_apply
deleted def Pmf.map
deleted theorem Pmf.map_apply
deleted theorem Pmf.map_bind
deleted theorem Pmf.map_comp
deleted theorem Pmf.map_const
deleted theorem Pmf.map_id
deleted theorem Pmf.mem_support_map_iff
deleted theorem Pmf.mem_support_seq_iff
deleted theorem Pmf.monad_map_eq_map
deleted theorem Pmf.monad_seq_eq_seq
deleted def Pmf.normalize
deleted theorem Pmf.normalize_apply
deleted def Pmf.ofFinset
deleted theorem Pmf.ofFinset_apply
deleted def Pmf.ofFintype
deleted theorem Pmf.ofFintype_apply
deleted theorem Pmf.pure_map
deleted def Pmf.seq
deleted theorem Pmf.seq_apply
deleted theorem Pmf.support_bernoulli
deleted theorem Pmf.support_filter
deleted theorem Pmf.support_map
deleted theorem Pmf.support_normalize
deleted theorem Pmf.support_ofFinset
deleted theorem Pmf.support_ofFintype
deleted theorem Pmf.support_seq
deleted theorem Pmf.toMeasure_map_apply
added theorem PMF.integral_eq_sum
added theorem PMF.integral_eq_tsum
deleted theorem Pmf.bernoulli_expectation
deleted theorem Pmf.integral_eq_sum
deleted theorem Pmf.integral_eq_tsum
added def PMF.bind
added theorem PMF.bindOnSupport_comm
added theorem PMF.bindOnSupport_pure
added theorem PMF.bind_apply
added theorem PMF.bind_bind
added theorem PMF.bind_comm
added theorem PMF.bind_const
added theorem PMF.bind_pure
added def PMF.pure
added theorem PMF.pure_apply
added theorem PMF.pure_apply_of_ne
added theorem PMF.pure_apply_self
added theorem PMF.pure_bind
added theorem PMF.pure_bindOnSupport
added theorem PMF.support_bind
added theorem PMF.support_pure
added theorem PMF.toMeasure_pure
added theorem PMF.toPMF_dirac
deleted def Pmf.bind
deleted def Pmf.bindOnSupport
deleted theorem Pmf.bindOnSupport_apply
deleted theorem Pmf.bindOnSupport_comm
deleted theorem Pmf.bindOnSupport_eq_bind
deleted theorem Pmf.bindOnSupport_pure
deleted theorem Pmf.bind_apply
deleted theorem Pmf.bind_bind
deleted theorem Pmf.bind_comm
deleted theorem Pmf.bind_const
deleted theorem Pmf.bind_pure
deleted theorem Pmf.mem_support_bind_iff
deleted theorem Pmf.mem_support_pure_iff
deleted def Pmf.pure
deleted theorem Pmf.pure_apply
deleted theorem Pmf.pure_apply_of_ne
deleted theorem Pmf.pure_apply_self
deleted theorem Pmf.pure_bind
deleted theorem Pmf.pure_bindOnSupport
deleted theorem Pmf.support_bind
deleted theorem Pmf.support_bindOnSupport
deleted theorem Pmf.support_pure
deleted theorem Pmf.toMeasure_bind_apply
deleted theorem Pmf.toMeasure_pure
deleted theorem Pmf.toMeasure_pure_apply
deleted theorem Pmf.toPmf_dirac
added def PMF.ofMultiset
added theorem PMF.ofMultiset_apply
added theorem PMF.support_ofMultiset
deleted def Pmf.ofMultiset
deleted theorem Pmf.ofMultiset_apply
deleted theorem Pmf.support_ofMultiset
deleted def Pmf.uniformOfFinset
deleted theorem Pmf.uniformOfFinset_apply