proposition: Lemma entropy_head_of1 (A : finType) (P : {fdist 'M[A]_1}) : `H P = `H (head_of_fdist_rV P).
proof: Proof. rewrite /entropy; congr (- _); apply: big_rV_1 => // a. rewrite /head_of_fdist_rV fdist_fstE /= big_rV0_row_of_tuple fdist_prod_of_rVE/=; congr (P _ * log (P _)); apply/rowP => i. by rewrite (ord1 i) !mxE; case: splitP => // i0; rewrite (ord1 i0) mxE. by rewrite (ord1 i) !mxE; case: splitP => // i0; rewrite (ord1 i0) mxE. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence