fact: Definition sum_mlog_prod (A : finType) (P : {fdist A}) n : {RV (P `^ n) -> R} := (fun t => \sum_(i < n) - log (P t ``_ i))%R.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext bigop_ext ssralg_ext logb fdist proba entropy