proposition: Lemma affine_function_Sum (A B : convType) (f : {affine A -> B}) (n : nat) (g : 'I_n -> A) (e : {fdist 'I_n}) : f (<|>_e g) = <|>_e (f \o g).
proof: Proof. elim: n g e => [g e|n IH g e]; first by move: (fdistI0_False e). have [/eqP|e10] := eqVneq (e ord0) 1%coqR. by rewrite fdist1E1 => /eqP ->; rewrite 2!Convn_fdist1. by rewrite 2!convnE affine_conv IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex