proposition: Lemma ssum_fdist_convn : \ssum_(i < n) scalept (p i) (\ssum_(j <- enum B) scalept (q i j) (h j)) = \ssum_(j <- enum B) scalept (fdist_convn p q j) (h j).
proof: Proof. transitivity (\ssum_i \ssum_(i0 <- enum B) scalept (p i) (scalept (q i i0) (h i0))). by apply eq_bigr => i _; rewrite big_morph_scalept// scalept0. rewrite exchange_big /=; apply eq_bigr => j _; rewrite fdist_convnE. have HF i : (0 <= p i * q i j)%coqR by exact/mulR_ge0. rewrite (scalept_sum _ (mkNNFun HF)) /=; apply eq_bigr => i _. by rewrite scaleptA. 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