proposition: Lemma Convn_of_fsdistmap (C D : convType) (f : {affine C -> D}) (d : {dist C}) : f (Convn_of_fsdist d) = Convn_of_fsdist (fsdistmap f d).
proof: Proof. apply S1_inj => /=. rewrite S1_proj_Convn_finType // S1_Convn_finType. set X := LHS. under eq_bigr do rewrite fdist_of_fsE. rewrite ssum_seq_finsuppE' supp_fsdistmap. under eq_bigr do rewrite fsdistbindE. rewrite big_seq; under eq_bigr=> y Hy. - rewrite big_scaleptl'; [| by rewrite scale0pt | by move=> j; apply mulR_ge0]. under eq_bigr=> i do rewrite fsdist1E inE. over. rewrite -big_seq exchange_big /=. rewrite (@big_seq _ _ _ _ (finsupp d)). under eq_bigr=> x Hx. - rewrite (big_fsetD1 (f x)) /=; last by apply/imfsetP; exists x. rewrite eqxx mulR1. rewrite (@big_seq _ _ _ _ ([fset f x0 | x0 in finsupp d] `\ f x)). under eq_bigr=> y do [rewrite in_fsetD1=> /andP [] /negbTE -> Hy; rewrite mulR0 scale0pt]. rewrite big1 // addpt0. over. rewrite /X. under eq_bigr do rewrite fdist_of_fsE. by rewrite ssum_seq_finsuppE'' big_seq. 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