fact: Definition fsdistmapE (A B : choiceType) (f : A -> B) (d : {dist A}) b : fsdistmap f d b = \sum_(a <- finsupp d | f a == b) d a.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex