proposition: Lemma Convn_of_fsdist_affine : affine Convn_of_fsdist.
proof: Proof. move=> p x y. have [->|pn0] := eqVneq p 0%:pr; first by rewrite !conv0. have [->|pn1] := eqVneq p 1%:pr; first by rewrite !conv1. have opn0 : (Prob.p p).~ != R0. by apply onem_neq0. apply: S1_inj; rewrite affine_conv/= !S1_Convn_finType ssum_seq_finsuppE. under [LHS]eq_bigr do rewrite fsdist_scalept_conv. rewrite big_seq_fsetE big_scalept_conv_split /=. rewrite 2!ssum_seq_finsuppE' 2!ssum_seq_finsuppE. rewrite -(@ssum_widen_finsupp x); last exact/finsupp_conv_subr. by rewrite -(@ssum_widen_finsupp y)//; exact/finsupp_conv_subl. 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