proposition: Lemma P_fssum A : P A = (\sum_(i \in A `&` [set` finsupp d]) (d i)%:E)%E.
proof: Proof. rewrite P_fssum'. by rewrite esum_fset; [| exact: finite_setIr | by move=> *; exact: d0]. Qed.
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 mathcomp(measure probability)