proposition: Lemma sum_mlog_prod_sum_map_mlog (A : finType) (P : {fdist A}) n : sum_mlog_prod P n.+1 \=sum (\row_(i < n.+1) `-- (`log P)).
proof: Proof. elim : n => [|n IH]. - move: (@sum_n_1 A P (\row_i `-- (`log P))). set mlogP := cast_fun_rV10 _. move => HmlogP. set mlogprodP := @sum_mlog_prod _ _ 1. suff -> : mlogprodP = mlogP by []. rewrite /mlogprodP /mlogP /sum_mlog_prod /cast_fun_rV10 /= mxE /=. by rewrite boolp.funeqE => ta; rewrite big_ord_recl big_ord0 addR0. - rewrite [X in _ \=sum X](_ : _ = row_mx (\row_(i < 1) (`-- (`log P))) (\row_(i < n.+1) `-- (`log P))); last first. apply/rowP => b; rewrite !mxE; case: splitP. by move=> a; rewrite {a}(ord1 a) => _; rewrite mxE. by move=> k _; rewrite mxE. apply: (sum_n_cons IH _) => /= ta. rewrite /sum_mlog_prod /= big_ord_recl /=; congr (_ + _)%R. by apply eq_bigr => i _; rewrite mxE. Qed.
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