proposition: Lemma ConvnDlr n m (p : {prob R}) (f : 'I_n -> T) (d : {fdist 'I_n}) (g : 'I_m -> T) (e : {fdist 'I_m}) : <|>_d f <|p|> <|>_e g = <|>_(fdist_add d e p) (fun i => match fintype.split i with inl i => f i | inr i => g i end).
proof: Proof. apply: S1_inj; rewrite affine_conv/= 3!S1_Convn convptE. do 2 rewrite big_morph_scalept ?scalept0//. rewrite big_split_ord/=. congr addpt; apply: congr_big => //= i _; rewrite scaleptA// fdist_addE. - case: fintype.splitP => [j/= /ord_inj ->//|k/= ink]. by have := ltn_ord i; rewrite ink -ltn_subRL subnn. - case: fintype.splitP => [j/= nij|k/=/eqP/[!eqn_add2l]/eqP/ord_inj ->//]. by have := ltn_ord j; by rewrite -nij -ltn_subRL subnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist