Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-29 15:08 4f9e951f

View on Github →

feat(analysis): add probability mass functions

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.sum_nat_cast

added theorem multiset.to_finset_sum_count_eq

Modified analysis/ennreal.lean

added theorem ennreal.coe_eq_coe

added theorem ennreal.coe_mul

added theorem ennreal.coe_one

added theorem ennreal.tendsto_coe_iff

added theorem ennreal.tendsto_of_real_iff

added theorem has_sum_of_nonneg_of_le

added theorem nnreal.has_sum_of_le

Modified analysis/nnreal.lean

added theorem nnreal.has_sum_coe

added theorem nnreal.is_sum_coe

added theorem nnreal.sum_coe

added theorem nnreal.tendsto_coe

Created analysis/probability_mass_function.lean

added def pmf.bind

added theorem pmf.bind_apply

added theorem pmf.bind_bind

added theorem pmf.bind_comm

added theorem pmf.bind_pure

added theorem pmf.bind_pure_comp

added theorem pmf.coe_bind_apply

added theorem pmf.coe_le_one

added theorem pmf.has_sum_coe

added theorem pmf.is_sum_coe_one

added def pmf.map

added theorem pmf.map_comp

added theorem pmf.map_id

added def pmf.of_multiset

added def pmf.pure

added theorem pmf.pure_apply

added theorem pmf.pure_bind

added theorem pmf.pure_map

added def pmf.seq

added def pmf.support

added theorem pmf.tsum_coe

added def {u}

Modified analysis/topology/infinite_sum.lean

added theorem is_sum_iff_of_has_sum

added theorem is_sum_ite

added theorem tsum_ite

Modified data/finset.lean

added theorem multiset.to_finset_cons

Modified data/multiset.lean

modified theorem multiset.count_eq_zero_of_not_mem

Modified order/filter.lean

added theorem filter.le_of_map_le_map_inj_iff