proposition: Lemma xlnx_entropy (P : {fdist A}) : `H P = / ln 2 * - \sum_(a : A) xlnx (P a).
proof: Proof. rewrite /entropy mulRN; congr (- _); rewrite big_distrr/=. apply: eq_bigr => a _; rewrite /log /Rdiv mulRA mulRC; congr (_ * _). rewrite /xlnx; case : ifP => // /RltP Hcase. have -> : P a = 0 by case (Rle_lt_or_eq_dec 0 (P a)). by rewrite mul0R. 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