proposition: Lemma supp_fsdist_convn : finsupp (<|>_e g) = \big[fsetU/fset0]_(i < n | (0 < e i)%mcR) finsupp (g i).
proof: Proof. apply/fsetP => a; apply/idP/idP => [|]; rewrite mem_finsupp fsdist_convnE. case/sumR_neq0 => /=; first by move=> ?; apply: mulR_ge0. move=> j [] /= ? eg0. apply/bigfcupP. exists j; first by apply/andP; split=> //; exact/RltP/(pmulR_lgt0' eg0). rewrite mem_finsupp gtR_eqF //. exact/(pmulR_rgt0' eg0). case/bigfcupP=> j /andP [] ? /RltP ? /[!mem_finsupp] /prob_gt0 /= ?. apply/sumR_neq0; first by move=> ?; apply/mulR_ge0. by exists j; split=> //; apply/mulR_gt0 => //; exact/RltP. 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